Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Komplexität und Kryptografie

Nondeterministic instance complexity and hard-to-prove tautologies

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.

Ps-File: Nondeterministic instance complexity and hard-to-prove tautologies