Abstract
Vikraman Arvind, Johannes Köbler, Martin Mundhenk and Jacobo Torán
Abstract:
In this note we first formalize the notion of hard tautologies using a
nondeterministic generalization of instance complexity. We then show,
under reasonable complexity-theoretic assumptions, that there are infinitely
many propositional tautologies that are hard to prove in any sound
propositional proof system.