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.
CITATION STYLE
Arvind, V., Köbler, J., Mundhenk, M., & Torán, J. (2000). Nondeterministic instance complexity and hard-to-prove tautologies. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1770, pp. 314–323). Springer Verlag. https://doi.org/10.1007/3-540-46541-3_26
Mendeley helps you to discover research relevant for your work.