On lengths of proofs in propositional calculi
Project/Area Number  13680422 
Research Category 
GrantinAid for Scientific Research (C)

Allocation Type  Singleyear Grants 
Section  一般 
Research Field 
計算機科学

Research Institution  National Institute of Informatics 
Principal Investigator 
ARAI Noriko National Institute of Informatics, Foundation of Informatics Research Division, Associate Professor, 情報学基礎研究系, 助教授 (40264931)

Project Period (FY) 
2001 – 2003

Project Status 
Completed(Fiscal Year 2003)

Budget Amount *help 
¥3,000,000 (Direct Cost : ¥3,000,000)
Fiscal Year 2003 : ¥700,000 (Direct Cost : ¥700,000)
Fiscal Year 2002 : ¥900,000 (Direct Cost : ¥900,000)
Fiscal Year 2001 : ¥1,400,000 (Direct Cost : ¥1,400,000)

Keywords  Proof complexity / Computational complexity / Logic / Propositional logic / 複雑さ理論 / 数学基礎論 / 自動証明 / resolution / tableau / 証明論 / 計算の複雑さ理論 / 証明の複雑さ理論 / 遠隔教育 
Research Abstract 
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 pigeonhole principle) found to be exponentially hard for resolution. In SCR, we have polynomialsize proofs for some of these hard combinatorial problems. We implementer SCR as a theorem prover, Godzilla. We showed that Godzilla proves the pigeonhole principle, kclique coloring, modk 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

Report
(4results)
Research Products
(12results)