Skip to main content
SpringerLink
Log in

Applications of CERES

  • Chapter
  • First Online:
Methods of Cut-Elimination

Part of the book series: Trends in Logic ((TREN,volume 34))

  • 610 Accesses

Abstract

CERES has applications to complexity theory, proof theory and to general mathematics. We first characterize classes of proofs which admit fast cut-elimination due to the resulting structure of the characteristic clause sets. Furthermore CERES can be applied to the efficient constructions of interpolants in classical logic and other logics for which CERES-methods can be defined. CERES is also suitable for calculating most general proofs from proof examples. Finally we demonstrate that CERES is also an efficient tool for the in-depth analysis of mathematical proofs.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    The C++ Programming Language following the International Standard 14882:1998 approved as an American National Standard (see http://www.ansi.org).

  2. 2.

    The current version of ceres uses the automated theorem prover Prover9 (see http://www.cs.unm.edu/mccune/mace4/), but any refutational theorem prover capable of paramodulation may be used.

  3. 3.

    See http://www.w3.org/XML/ for more information on the Extensible Markup Language specification.

  4. 4.

    http://www.logic.at/ceres/

  5. 5.

    HLK Website: http://www.logic.at/hlk/

  6. 6.

    ProofTool Website: http://www.logic.at/prooftool/

References

  1. M. Aigner, G.M. Ziegler: Proofs from THE BOOK. Springer, Berlin, 1998.

    MATH  Google Scholar 

  2. P.B. Andrews: Resolution in Type Theory. Journal of Symbolic Logic, 36, pp. 414–432, 1971.

    Article  MathSciNet  MATH  Google Scholar 

  3. M. Baaz, S. Hetzl, A. Leitsch, C. Richter, H. Spohr: Cut-Elimination: Experiments with CERES. Proceedings of LPAR 2004, Lecture Notes in Computer Science 3452, pp. 481–495, 2005.

    Google Scholar 

  4. M. Baaz, S. Hetzl, A. Leitsch, C. Richter, H. Spohr: Proof Transformation by CERES. In: J.M. Borwein, W.M. Farmer (eds.), MKM 2006, LNCS (LNAI), vol. 4108, pp. 82–93. Springer, Heidelberg, 2006.

    Google Scholar 

  5. M. Baaz, S. Hetzl, A. Leitsch, C. Richter, H. Spohr: CERES: An Analysis of Fürstenberg’s Proof of the Infinity of Primes. Theoretical Computer Science, 403 (2–3), pp. 160–175, 2008.

    Article  MathSciNet  MATH  Google Scholar 

  6. M. Baaz, A. Leitsch: Cut Normal Forms and Proof Complexity. Annals of Pure and Applied Logic, 97, pp. 127–177, 1999.

    Article  MathSciNet  MATH  Google Scholar 

  7. M. Baaz, A. Leitsch: Towards a Clausal Analysis of Cut-Elimination. Journal of Symbolic Computation, 41, pp. 381–410, 2006.

    Article  MathSciNet  MATH  Google Scholar 

  8. M. Baaz, P. Pudlak: Kreisel’s Conjecture for LE1. In: P. Clote, J. Krajicek (eds.), Arithmetic Proof Theory and Computational Complexity, Oxford University Press, Oxford, pp. 30–49, 1993.

    Google Scholar 

  9. M. Baaz, P. Wojtylak: Generalizing Proofs in Monadic Languages. Annals of Pure and Applied Logic, 154(2): 71–138, 2008.

    Article  MathSciNet  MATH  Google Scholar 

  10. E. Börger, E. Grädel, Y. Gurevich: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Berlin, 1997.

    Google Scholar 

  11. J.Y. Girard: Proof Theory and Logical Complexity. In Studies in Proof Theory, Bibliopolis, Napoli, 1987.

    Google Scholar 

  12. S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo: Herbrand Sequent Extraction. AISC/Calculemus/MKM 2008, LNAI 5144, pp. 462–477, 2008.

    Google Scholar 

  13. S. Hetzl, A. Leitsch, D. Weller, B. Woltzenlogel Paleo: Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions. Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics, CEUR Workshop Proceedings, vol 378, ISSN 1613-0073, 2008.

    Google Scholar 

  14. W.H. Joyner: Resolution Strategies as Decision Procedures. Journal of the ACM, 23(1), pp. 398–417, 1976.

    Article  MathSciNet  MATH  Google Scholar 

  15. U. Kohlenbach: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. In Springer Monographs in Mathematics, Springer, Berlin, 2009.

    Google Scholar 

  16. C.J. Krajicek, P. Pudlak: The Number of Proof Lines and the Size of Proofs in First Order Logic. Archive for Mathematical Logic, 27, pp. 69–84, 1988.

    Article  MathSciNet  MATH  Google Scholar 

  17. A. Leitsch: The Resolution Calculus. EATCS Texts in Theoretical Computer Science. Springer, Berlin, 1997.

    Google Scholar 

  18. H. Luckhardt: Herbrand-Analysen zweier Beweise des Satzes von Roth: polynomiale Anzahlschranken. Journal of Symbolic Logic, 54, pp. 234–263, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  19. G. Mints: Quick Cut-Elimination for Monotone Cuts. In Games, Logic, and Constructive Sets, The University of Chicago Press, Chicago, IL, 2003.

    Google Scholar 

  20. V.P. Orevkov: Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Journal of Soviet Mathematics, 20, pp. 2337–2350, 1982.

    Article  MATH  Google Scholar 

  21. W.W. Tait: Normal Derivability in Classical Logic. In: J. Barwise (ed.), The Syntax and Semantics of Infinitary Languages, Springer, Berlin, pp. 204–236, 1968.

    Chapter  Google Scholar 

  22. G. Takeuti: Proof Theory. North-Holland, Amsterdam, 2nd edition, 1987.

    Google Scholar 

  23. C. Urban: Classical Logic and Computation. PhD Thesis, University of Cambridge Computer Laboratory, 2000.

    Google Scholar 

  24. B. Woltzenlogel Paleo: Herbrand Sequent Extraction. VDM Verlag Dr.Müller e.K., Saarbrücken, , ISBN-10: 3836461528, February 7, 2008.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Vienna University of Technology, Wiedner Hauptstraße 8-10, 1040, Vienna, Austria

    Matthias Baaz

  2. Vienna University of Technology, Favoritenstraße 9, 1040, Vienna, Austria

    Alexander Leitsch

Authors
  1. Matthias Baaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Leitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthias Baaz .

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Baaz, M., Leitsch, A. (2011). Applications of CERES. In: Methods of Cut-Elimination. Trends in Logic, vol 34. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0320-9_8

Download citation

Publish with us

Policies and ethics

Search

Navigation