Sciweavers

Share
AML
2006

Upper bounds on complexity of Frege proofs with limited use of certain schemata

8 years 4 months ago
Upper bounds on complexity of Frege proofs with limited use of certain schemata
The paper considers a commonly used axiomatization of the classical propositional logic and studies how different axiom schemata in this system contribute to proof complexity of the logic. The existence of a polynomial bound on proof complexity of every statement provable in this logic is a well-known open question. The axiomatization consists of three schemata. We show that any statement provable using unrestricted number of axioms from the first of the three schemata and polynomially-bounded in size set of axioms from the other schemata, has a polynomially-bounded proof complexity. In addition, it is also established, that any statement, provable using unrestricted number of axioms from the remaining two schemata and polynomially-bounded in size set of axioms from the first scheme, also has a polynomially-bounded proof complexity.
Pavel Naumov
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2006
Where AML
Authors Pavel Naumov
Comments (0)
books