On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT

Abstract. For a reasonable sound and complete proof calculus for firstorder logic consider the problem to decide, given a sentence of firstorder logic and a natural number n, whether has no proof of length n. We show that there is a nondeterministic algorithm accepting this problem which, for fixed , has running time bounded by a polynomial in n if and only if there is an optimal proof system for the set TAUT of tautologies of propositional logic. This equivalence is an instance of a general result linking the complexity of so-called slicewise monotone parameterized problems with the existence of an optimal proof system for TAUT.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Yijia Chen, Jörg Flum
• Keywords: Automated Reasoning, Complete Proof Calculus, CSL 2010, Firstorder Logic, Optimal Proof