On lengths of proofs in propositional calculi

论命题演算中证明的长度

• 批准号: 13680422
• 负责人: ARAI Noriko
• 金额: $ 1.92万
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13680422/
• 关键词: Proof complexity; Computational complexity; Logic; Propositional logic; 複雑さ理論; 数学基礎論; 自動証明; resolution; tableau; 証明論; 計算の複雑さ理論; 証明の複雑さ理論; 遠隔教育

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

计算机科学中最基本的问题之一是寻找最有效的算法来计算给定的函数。计算的相对效率问题通常由一个著名的公开问题P=NP来表示。有没有什么问题多项式时间可以被一个非确定的图灵机识别，而不是一个确定的图灵机？首先要做的工作是获得命题逻辑的各种系统的详细映射。它具有两种不同的研究类型：1.在命题演算中找出需要超多项式证明的重言式序列.2.检验两个命题演算在多项式型中是否可互译.在我们的研究中，我们彻底解决了各种类型的解析表的相对效率及其相对于归结系统的相对效率的问题.需要指出的是，解析表和归结是采用最多的命题演算。经常以…的身份更是自动化定理证明器的基础。自1970年S以来，人们一直认为著名的解析表具有与一般解析表相同的效率，但我们证明了一般解析表相对于子句表具有超多项式加速比。此外，我们还证明了归结在一般分析表上只有超多项式加速比，尽管人们认为归结在分析表上具有指数加速比.在子句分析表的基础上，我们增加了一条称为对称规则的推理规则，构造了一种新的命题演算--简单组合推理.有许多组合定理(即鸽子洞原理)被发现是指数级难以解决的。在SCR中，我们对其中一些困难的组合问题有多项式大小的证明。我们实现了SCR作为一个定理证明器，哥斯拉。我们证明了哥斯拉在多项式时间内证明了鸽子洞原理、k-团染色、mod-k原理和Bondy定理。同时，我们证明了哥斯拉证明随机生成的3CNF需要指数时间，这是预期的结果，因为我们不能期望随机生成的公式有多大的对称性。较少

项目成果

Arai, Pitassi, Urquhart: "The complexity of analytic tableaux"Proceedings of ACM Symposium of Theory of Computing 2001. 356-363 (2001)

Arai、Pitassi、Urquhart：“分析画面的复杂性”ACM 计算理论研讨会论文集 2001。 356-363 (2001)

Noriko H.Arai, Toniann Pittasi, Alasdair Urquhart: "The complexity of analytic tableaux"Proceedings of Symposium of Theory of Computing (STOC'01). 356-363 (2001)

Noriko H.Arai、Toniann Pittasi、Alasdair Urquhart：“分析画面的复杂性”计算理论研讨会论文集 (STOC01)。

N.Arai, T.Pittassi, A.Urquhart: "The complexity of analytic tableaux"Proceedings of STOC2001 (Symposium of Theory of Computing). 356-363 (2001)

N.Arai、T.Pittassi、A.Urquhart：“分析画面的复杂性”STOC2001（计算理论研讨会）论文集。