On lengths of proofs in propositional calculi

计算机科学中最基本的问题之一是找到计算给定函数的最有效算法。问题的相对效率的计算往往代表著名的开放式问题，P=？NP问题是否存在多项式时间内可被非确定图灵机识别而不可被确定图灵机识别的问题？要做的第一项工作是获得各种命题逻辑系统的详细地图。它的特点是两种不同类型的研究：1.在一个命题演算中寻找一个需要超多项式证明的重言式序列; 2.检验两个命题演算在多项式时间内是否可相互平移.在我们的研究中，我们彻底解决了各种类型的解析表的相对效率问题，以及它对归结系统的相对效率问题.值得注意的是，分析表和归结是采用最多的命题演算。频繁 ...更多信息 自动定理证明器的基础。自20世纪70年代以来，人们一直认为分析表具有与一般分析表相同的效率，本文称之为子句表。然而，我们发现，一般的分析表有超多项式加速子句表。此外，我们还证明了归结在一般解析表上只有超多项式加速比，而在一般解析表上归结只有指数加速比.在子句解析表的基础上，我们增加了一个推理规则，称为对称规则，构造了一个新的命题演算，称为简单组合推理（Simple Combinatorial Reasoning，SCR）.有许多组合定理（即鸽子洞原理）被发现是指数难以解决的。在SCR中，我们对这些困难的组合问题中的一些进行了多项式大小的证明。我们实现SCR作为一个定理证明，哥斯拉。我们证明了Godzilla在多项式时间内证明了鸽子洞原理、k-团染色、mod-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