Paper Info
Title
Does Advice Help to Prove Propositional Tautologies?
Abstract
One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [6], where they defined propositional proof systems as poly-time computable functions which have all propositional tautologies as their range. Motivated by provability consequences in bounded arithmetic, Cook and Krajíček [5] have recently started the investigation of proof systems which are computed by poly-time functions using advice. While this yields a more powerful model, it is also less directly applicable in practice. In this note we investigate the question whether the usage of advice in propositional proof systems can be simplified or even eliminated. While in principle, the advice can be very complex, we show that proof systems with logarithmic advice are also computable in poly-time with access to a sparse NP-oracle. In addition, we show that if advice is ”not very helpful” for proving tautologies, then there exists an optimal propositional proof system without advice. In our main result, we prove that advice can be transferred from the proof to the formula, leading to an easier computational model. We obtain this result by employing a recent technique by Buhrman and Hitchcock [4].
Year
DOI
Venue
2009
10.1007/978-3-642-02777-2_8
Theory and Applications of Satisfiability Testing
Keywords
Field
DocType
advice help,main result,poly-time computable function,poly-time function,prove propositional tautologies,propositional proof complexity,propositional proof system,logarithmic advice,easier computational model,optimal propositional proof system,proof system,propositional tautology,computer model
Discrete mathematics,Tautology (logic),Proof by contradiction,Existential quantification,Computer science,Propositional proof system,Proof complexity,Well-formed formula,Computable function,Propositional variable
Conference
Volume
ISSN
Citations 
5584
0302-9743
2
PageRank 
References 
Authors
0.38
7
2
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Sebastian Müller271.20