One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow (JSL 79), where they definedpropositional proof systems as poly-time computable functions which have all propositional tautologies as their range. Motivated by provability consequences in bounded arithmetic, Cook and Krajicek (JSL 07) 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 a 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 Krajicek gave a surprising positive answer which we extend to all languages.

These results show that using advice yields a more powerful model, but it 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'08) we also manage to transfer the advice from the proof to the formula, which leads to an easier computational model.