Name
Abstract | ||
|---|---|---|
One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [J. Symbolic Logic, 1979], 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 Kraji'cek [J. Symbolic Logic, 2007] have recently started the investigation of proof systems which are computed by poly-time functions using advice. In this paper we concentrate on three fundamental questions regarding this new model. First, we investigate whether a given language L admits a polynomially bounded proof system with advice. Depending on the complexity of the underlying language L and the amount and type of the advice used by the proof system, we obtain different characterizations for this problem. In particular, we show that this question is tightly linked with the question whether L has small nondeterministic instance complexity. The second question concerns the existence of optimal proof systems with advice. For propositional proof systems, Cook and Kraji'cek gave a surprising positive answer which we extend to all languages. These results show that providing proof systems with advice yields a more powerful model, but this model is also less directly applicable in practice. Our third question therefore asks 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 propositional proof systems with logarithmic advice are also computable in poly-time with access to a sparse NP-oracle. Employing a recent technique of Buhrman and Hitchcock [CCC, 2008] we also manage to transfer the advice from the proof to the proven formula, which leads to a more practical computational model. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.ic.2010.11.006 | Inf. Comput. |
Keywords | DocType | Volume |
j. symbolic logic,polynomially bounded proof systems,computational complexity,polynomially bounded proof system,advice yield,propositional proof system,propositional proof complexity,advice,logarithmic advice,optimal proof systems,proof system,propositional tautology,optimal proof system,fundamental question,proof systems,instance complexity,computer model | Journal | 209 |
Issue | ISSN | Citations |
3 | Information and Computation | 3 |
PageRank | References | Authors |
0.39 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olaf Beyersdorff | 1 | 223 | 30.33 |
| Johannes Köbler | 2 | 580 | 46.51 |
| Sebastian Müller | 3 | 63 | 13.40 |