Sciweavers

Share
CSL
2010
Springer

On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT

8 years 4 months ago
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.
Yijia Chen, Jörg Flum
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Yijia Chen, Jörg Flum
Comments (0)
books