On lengths of proofs in propositional calculi

计算机科学中最基本的问题之一是找到最有效的算法来计算给定的函数。计算的相对效率问题通常由著名的开放问题P=？NP问题是否存在一个多项式时间的问题可以被非确定性图灵机识别而不能被任何确定性图灵机识别？要做的第一件事是获得命题逻辑的各种系统的详细地图。它有两种不同的研究类型：1。在命题演算中找到需要超多项式证明的重言式序列。检验两个命题演算在多项式时间内是否可译。在我们的研究中，我们彻底解决了各种类型的分析表的相对效率问题，以及它对分辨率系统的相对效率问题。需要注意的是，解析表法和解析法是采用最多的命题演算法。更多的是自动定理证明的基础。自20世纪70年代以来，人们一直认为著名的分析表具有与一般分析表相同的效率，本文将其称为小句表。然而，我们证明了一般解析表比子句表具有超多项式加速。此外，我们证明了分辨率在一般解析表上只有超多项式加速，尽管人们认为分辨率在解析表上有指数加速。在子句解析表的基础上，我们增加了一个叫做对称规则的推理规则，构造了一个新的命题演算——简单组合推理（SCR）。有许多组合定理（如鸽子洞原理）被发现很难用指数来解决。在SCR中，我们对这些困难的组合问题有多项式大小的证明。我们实现SCR作为定理证明者，哥斯拉。证明了Godzilla在多项式时间内证明了鸽子洞原理、k-团着色、k-模原理和邦迪定理。同时，我们证明了Godzilla需要指数时间来证明随机生成的3CNF，这是预期的结果，因为我们不能期望随机生成的公式有太多的对称性。少

One of the most fundamental questions in computer science asks to find the most efficient algorithm to compute a given function. The question of relative efficiency of computation often represented by the famous open question, P=?NP problem is there any problem polynomial time recognizable by a nondeterministic Turing Machine but not by ay deterministic Turing Machine?The first job to be done is to obtain a detailed map of various systems of propositional logic. It features two different types of study:1.To find a sequence of tautologies which requires susperpolynomial proofs in a propositional calculus.2.To check whether or not two propositional calculi are translatable each other in polynomial tyme.In our research, we thoroughly solved the question of relative efficiency of various types of analytic tableaux, and its relative efficiency to the system of resolution. It should be noted that analytic tableaux and resolution are the propositional calculi which adopted most. frequently as … More the basis of automated theorem provers. The well known analytic tableau, which is named clausal tableau in our paper, had been believed to have the same efficiency with general analytic tableau since 1970's. However, we showed that general analytic tableau has superpolynomial speedup over clausal tableau. Moreover, we showed that resolution has only superpolynomial speedup over general analytic tableau, although it had been believed that resolution had exponential speedup over analytic tableaux.Based on clausal analytic tableau, we add an inference rule called symmetry 'rule to construct a new propositional calculus called Simple Combinatorial Reasoning (SCR). There are numerous combinatorial theorems (i.e. the pigeon-hole principle) found to be exponentially hard for resolution. In SCR, we have polynomial-size proofs for some of these hard combinatorial problems. We implementer SCR as a theorem prover, Godzilla. We showed that Godzilla proves the pigeon-hole principle, k-clique coloring, mod-k principle and Bondy's theorem in polynomial time. At the same time, we demonstrated that it takes exponential time for Godzilla to prove randomly generated 3CNF's, which was expected result since we cannot expect much symmetry in randomly generated formulas. Less