Abstract
For a reasonable sound and complete proof calculus for first-order logic consider the problem to decide, given a sentence ϕ of first-order 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chen, Y., Flum, J.: A logic for PTIME and a parameterized halting problem. In: Proceedings of the 24th IEEE Symposium on Logic in Computer Science (LICS 2009), pp. 397–406 (2009)
Chen, Y., Flum, J.: On the complexity of Gödel’s proof predicate. The Journal of Symbolic Logic 75(1), 239–254 (2010)
Chen, Y., Flum, J.: On p-optimal proof systems and logics for PTIME. In: Gavoille, C. (ed.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 321–332. Springer, Heidelberg (2010)
Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems. The Journal of Symbolic Logic 44, 36–50 (1979)
Ebbinghaus, H.-D., Flum, J.: Finite Model Theory, 2nd edn. Springer, Heidelberg (1999)
Gödel, K.: Collected Works, vol. VI, pp. 372–376. Clarendon Press, Oxford (2003)
Gurevich, Y.: Logic and the challenge of computer science. In: Current Trends in Theoretical Computer Science, pp. 1–57. Computer Science Press, Rockville (1988)
Köbler, J., Messner, J.: Complete problems for promise classes by optimal proof systems for test sets. In: Proceedings of the 13th IEEE Conference on Computational Complexity (CCC 1998), pp. 132–140 (1998)
Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. The Journal of Symbolic Logic 54, 1063–1088 (1989)
Messner, J.: On optimal algorithms and optimal proof systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 361–372. Springer, Heidelberg (1999)
Monroe, H.: Speedup for natural problems. Electronic Colloquium on Computational Complexity, Report TR09-056 (2009)
Nash, A., Remmel, J., Vianu, V.: PTIME queries revisited. In: Eiter, T., Libkin, L. (eds.) ICDT 2005. LNCS, vol. 3363, pp. 274–288. Springer, Heidelberg (2004)
Sadowski, Z.: On an optimal propositional proof system and the structure of easy subsets. Theoretical Computer Science 288(1), 181–193 (2002)
Vardi, M.Y.: On the complexity of bounded-variable queries. In: Proceedings of the 14th ACM Symposium on Principles of Database Systems (PODS 1995), pp. 266–276 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, Y., Flum, J. (2010). On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)