2003 Fiscal Year Final Research Report Summary
On lengths of proofs in propositional calculi
| Project/Area Number |
13680422
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year 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
|
| Keywords | Proof complexity / Computational complexity / Logic / Propositional logic |
|---|
| 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 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
|
