Skip to main content
SpringerLink
Log in

From Feasible Proofs to Feasible Computations

  • Conference paper
Computer Science Logic (CSL 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6247))

Included in the following conference series:

  • 875 Accesses

Abstract

We shall discuss several situations in which it is possible to extract from a proof, be it a proof in a first-order theory or a propositional proof, some feasible computational information about the theorem being proved. This includes extracting feasible algorithms, deterministic or interactive, for witnessing an existential quantifier, a uniform family of short propositional proofs of instances of a universal quantifier, or a feasible algorithm separating a pair of disjoint NP sets.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge University Press, Cambridge (2009)

    MATH  Google Scholar 

  2. Bonet, M.L., Pitassi, T., Raz, R.: On Interpolation and Automatization for Frege Proof Systems. SIAM J. of Computing 29(6), 1939–1967 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  3. Buss, S.R.: Bounded Arithmetic. Naples, Bibliopolis (1986)

    MATH  Google Scholar 

  4. Buss, S.R., Krajíček, J.: An application of boolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society 69(3), 1–21 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  5. Clote, P., Kranakis, E.: Boolean Functions and Models of Computation. Springer, Heidelberg (2002)

    Google Scholar 

  6. Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Proc. Logic, Methodology and Philosophy of Science, pp. 24–30. North-Holland, Amsterdam (1965)

    Google Scholar 

  7. Cook, S.A.: Feasibly constructive proofs and the propositional calculus. In: Proc. 7\(^{\mbox{th}}\) Annual ACM Symp. on Theory of Computing, pp. 83–97. ACM Press, New York (1975)

    Google Scholar 

  8. Cook, S.A., Nguyen, P.: Logical foundations of proof complexity. Cambridge U. Press, Cambridge (2009)

    Google Scholar 

  9. Cook, S.A., Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36–50 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  10. Jeřábek, E.: Dual weak pigeonhole principle, Boolean complexity, and derandomization. Annals of Pure and Applied Logic 129, 1–37 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  11. Kolodziejczyk, L., Nguyen, P., Thapen, N.: The provably total NP search problems of weak second order bounded arithmetic (2009) (preprint)

    Google Scholar 

  12. Krajíček, J.: Fragments of bounded arithmetic and bounded query classes. Transactions of the A.M.S. 338(2), 587–598 (1993)

    Article  MATH  Google Scholar 

  13. Krajíček, J.: Bounded arithmetic, propositional logic, and complexity theory. Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)

    Google Scholar 

  14. Krajíček, J.: Hardness assumptions in the foundations of theoretical computer science. Archive for Mathematical Logic 44(6), 667–675 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  15. Krajíček, J.: Proof complexity. In: Laptev, A. (ed.) European congress of mathematics (ECM), Stockholm, Sweden, June 27-July 2, pp. 221–231. European Mathematical Society, Zurich (2005)

    Chapter  Google Scholar 

  16. Krajíček, J.: A form of feasible interpolation for constant depth Frege systems. J. of Symbolic Logic 75(2), 774–784 (2010)

    Article  MATH  Google Scholar 

  17. Krajíček, J.: On the proof complexity of the Nisan-Wigderson generator based on a hard \(\mbox{NP } \cap \mbox{ coNP}\) function (submitted, March 2010) (preprint); Preliminary version in Electronic Colloquium on Computational Complexity, Rep. No.54 (2010)

    Google Scholar 

  18. Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. J. Symbolic Logic 54(3), 1063–1079 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  19. Krajíček, J., Pudlák, P.: Quantified Propositional Calculi and Fragments of Bounded Arithmetic. Zeitschr. f. Mathematikal Logik u. Grundlagen d. Mathematik, Bd. 36(1), 29–46 (1990)

    Article  MATH  Google Scholar 

  20. Krajíček, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S^1_2\) and EF. Information and Computation 140(1), 82–94 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  21. Krajíček, J., Pudlák, P., Sgall, J.: Interactive Computations of Optimal Solutions. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 48–60. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  22. Krajíček, J., Pudlák, P., Takeuti, G.: Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic 52, 143–153 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  23. Krajíček, J., Skelley, A., Thapen, N.: NP search problems in low fragments of bounded arithmetic. J. of Symbolic Logic 72(2), 649–672 (2007)

    Article  MATH  Google Scholar 

  24. Papadimitriou, C.: The Complexity of the Parity Argument and Other Inefficient proofs of Existence. J. of Computer and System Sciences 48(3), 498–532 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  25. Pudlák, P.: The lengths of proofs. In: Buss, S.R. (ed.) Handbook of Proof Theory, pp. 547–637. Elsevier, Amsterdam (1998)

    Chapter  Google Scholar 

  26. Pudlák, P.: Consistency and games - in search of new combinatorial principles. In: Stoltenberg-Hansen, V., Vaananen, J. (eds.) Proc. Logic Colloquium 2003, Helsinki. Assoc. for Symbolic Logic, pp. 244–281 (2006)

    Google Scholar 

  27. Pudlák, P.: Fragments of Bounded Arithmetic and the lengths of proofs. J. of Symbolic Logic 73(4), 1389–1406 (2008)

    Article  MATH  Google Scholar 

  28. Skelley, A., Thapen, N.: The provably total search problems of bounded arithmetic (preprint 2007) (revised March 2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics and Physics, Charles University, Sokolovská 83, 186 75, Prague, Czech Republic

    Jan Krajíček

Authors
  1. Jan Krajíček
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Laboratory, University of Cambridge, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  2. Formal Methods in Systems Engineering, Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Helmut Veith

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Krajíček, J. (2010). From Feasible Proofs to Feasible Computations. 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_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15205-4_3

  • 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)

Publish with us

Policies and ethics

Search

Navigation