Skip to main content
SpringerLink
Log in

Herbrand Sequent Extraction

  • Conference paper
Intelligent Computer Mathematics (CICM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5144))

Included in the following conference series:

Abstract

Computer generated proofs of interesting mathematical theorems are usually too large and full of trivial structural information, and hence hard to understand for humans. Techniques to extract specific essential information from these proofs are needed. In this paper we describe an algorithm to extract Herbrand sequents from proofs written in Gentzen’s sequent calculus LK for classical first-order logic. The extracted Herbrand sequent summarizes the creative information of the formal proof, which lies in the instantiations chosen for the quantifiers, and can be used to facilitate its analysis by humans. Furthermore, we also demonstrate the usage of the algorithm in the analysis of a proof of the equivalence of two different definitions for the mathematical concept of lattice, obtained with the proof transformation system CERES.

Supported by the Austrian Science Fund (project P19875) and by the Programme Alban (project E05M054053BR).

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. Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Ceres: An Analysis of Fürstenberg’s Proof of the Infinity of Primes. Theoretical Computer Science (to appear)

    Google Scholar 

  2. Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Cut-Elimination: Experiments with CERES. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 481–495. Springer, Heidelberg (2005)

    Google Scholar 

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

    Chapter  Google Scholar 

  4. Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundamenta Matematicae 20, 353–379 (1994)

    MATH  MathSciNet  Google Scholar 

  5. Baaz, M., Leitsch, A.: Cut normal forms and proof complexity. Annals of Pure and Applied Logic 97, 127–177 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  6. Baaz, M., Leitsch, A.: Cut-elimination and Redundancy-elimination by Resolution. Journal of Symbolic Computation 29(2), 149–176 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  7. Buss, S.R.: On Herbrand’s theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, p. 195. Springer, Heidelberg (1995)

    Google Scholar 

  8. Gentzen, G.: Untersuchungen über das logische Schließen. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland Publishing Company, Amsterdam (1969)

    Google Scholar 

  9. Gerhardy, P., Kohlenbach, U.: Extracting herbrand disjunctions by functional interpretation. Archive for Mathematical Logic 44(5) (2005)

    Google Scholar 

  10. Herbrand, J.: Recherches sur la théorie de la démonstration. Travaux de la Societé des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques 33 (1930)

    Google Scholar 

  11. Hetzl, S.: Characteristic Clause Sets and Proof Transformations. PhD thesis, Vienna University of Technology (2007)

    Google Scholar 

  12. Hetzl, S., Leitsch, A.: Proof transformations and structural invariance. In: Aguzzoli, S., Ciabattoni, A., Gerla, B., Manara, C., Marra, V. (eds.) ManyVal 2006. LNCS (LNAI), vol. 4460, pp. 201–230. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  14. Statman, R.: Lower bounds on Herbrand’s theorem. Proceedings of the American Mathematical Society 75, 104–107 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  15. Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications 19(1), 35–48 (2006)

    MATH  MathSciNet  Google Scholar 

  16. Paleo, B.W.: Herbrand sequent extraction. Master’s thesis, Technische Universitaet Dresden; Technische Universitaet Wien, Dresden, Germany, Wien, Austria (2007)

    Google Scholar 

  17. Paleo, B.W.: Herbrand Sequent Extraction. VDM-Verlag. Saarbruecken, Germany (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Languages (E185), Vienna University of Technology, FavoritenstraĂźe 9, 1040, Vienna, Austria

    Stefan Hetzl, Alexander Leitsch, Daniel Weller & Bruno Woltzenlogel Paleo

Authors
  1. Stefan Hetzl
    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

  3. Daniel Weller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Bruno Woltzenlogel Paleo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Serge Autexier John Campbell Julio Rubio Volker Sorge Masakazu Suzuki Freek Wiedijk

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B. (2008). Herbrand Sequent Extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds) Intelligent Computer Mathematics. CICM 2008. Lecture Notes in Computer Science(), vol 5144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85110-3_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85109-7

  • Online ISBN: 978-3-540-85110-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation