Skip to main content
SpringerLink
Log in

Presenting machine-found proofs

  • Session 3B
  • Conference paper
  • First Online:
Automated Deduction — Cade-13 (CADE 1996)

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

Included in the following conference series:

Abstract

This paper outlines an implemented system named PROVERB that transforms and abstracts machine-found proofs to natural deduction style proofs at an adequate level of abstraction and then verbalizes them in natural language. The abstracted proofs, originally employed only as an intermediate representation, also prove to be useful for proof planning and proving by analogy.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Peter B. Andrews. Transforming matings into natural deduction proofs. In Proc. of the 5th CADE, 1980.

    Google Scholar 

  2. Daniel Chester. The translation of formal proofs into English. AI, 7:178–216, 1976.

    Google Scholar 

  3. Andrew Edgar and Francis Jeffry Pelletier. Natural language explanation of natural deduction proofs. In Proc. of the first Conference of the Pacific Association for Computational Linguistics, 1993.

    Google Scholar 

  4. Gerhard Gentzen. Untersuchungen über das logische Schließen I. Math. Zeitschrift, 39:176–210, 1935.

    Article  Google Scholar 

  5. Xiaorong Huang and Armin Fiedler. Paraphrasing and aggregating argumentative text using text structure. In Proc. of 8th International Workshop on Natural Language Generation, 1996.

    Google Scholar 

  6. Xiaorong Huang et al. Ω-MKRP — a proof development environment. In Proc. of 12th CADE, 1994.

    Google Scholar 

  7. Xiaorong Huang. Planning argumentative texts. In Proc. of 15th International Conference on Computational Linguistics, 1994.

    Google Scholar 

  8. Xiaorong Huang. Reconstructing proofs at the assertion level. In Proc. of 12th CADE, 1994.

    Google Scholar 

  9. Xiaorong Huang. Translating machine-generated resolution proofs into ndproofs at the assertion level. In Proc. of PRICAI-96, 1996.

    Google Scholar 

  10. Christoph Lingenfelder. Transformation and Structuring of Computer Generated Proofs. PhD thesis, Universität Kaiserslautern, 1990.

    Google Scholar 

  11. Frank Pfenning. Proof Transformation in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität des Saarlandes, Postfach 15 11 50, D-66041, Saarbrücken, Germany

    Xiaorong Huang & Armin Fiedler

Authors
  1. Xiaorong Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Armin Fiedler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huang, X., Fiedler, A. (1996). Presenting machine-found proofs. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_83

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_83

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61511-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation