Skip to main content
SpringerLink
Log in
Book cover

International Conference on Typed Lambda Calculi and Applications

TLCA 1995: Typed Lambda Calculi and Applications pp 109–123Cite as

Extracting text from proofs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 902))

Abstract

In this paper, we propose a method for presenting formal proofs in an intelligible form. We describe a transducer from proof objects (λ-terms in the Calculus of Constructions) to pseudo natural language that has been implemented for the Coq system.

Part of this research was done when the third author was at ATT Bell Laboratories.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Magnusson, B. Nordström, The ALF proof editor and Us proof engine, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.

    Google Scholar 

  2. D. Chester, The translation of Formal Proofs into English, Artificial Intelligence 7 (1976), 261–278, 1976.

    Article  Google Scholar 

  3. A. Cohn, Proof Accounts in HOL, unpublished draft.

    Google Scholar 

  4. Y. Coscoy, Traductions de preuves en langage naturel pour le systeme Coq, Rapport de Stage, Ecole Polytechnique, 1994.

    Google Scholar 

  5. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-Mohring, B. Werner, The Coq Proof Assistant User's Guide, INRIA Technical Report no. 134, 1991.

    Google Scholar 

  6. Y. Bertot, the CtCoq Interface, available by ftp at babar.inria.fr: /pub/centaur/ctcoq.

    Google Scholar 

  7. N.G. de Bruijn, The Mathematical Vernacular, a language for Mathematics with typed sets in Proceedings from the Workshop on Programming Logic, P. Dybjer et al., Programming Methodology Group, Volume 37, University of Göteborg, 1987.

    Google Scholar 

  8. A. Edgar, F.J. Pelletier, Natural language explanation of Natural Deduction proofs, in Proceedings of the First Conference of the Pacific Association for Computational Linguistics, Simon Fraser University, 1993.

    Google Scholar 

  9. A. Felty, Proof explanation and revision, Technical Report, University of Pennsylvania MS-CIS-88-17, 1988.

    Google Scholar 

  10. G. Gentzen, Investigations into logical deduction, in “The collected papers of Gerhard Gentzen”, M.E. Szabo (Ed.), pp. 69–131, North Holland, 1969.

    Google Scholar 

  11. M.J.C. Gordon, T.F. Melham, HOL: a proof generating system for higher-order logic, Cambridge University Press, 1992.

    Google Scholar 

  12. X. Huang, Reconstructing Proofs at the Assertion Level, in Proceedings of CADE-12, Nancy, LNAI 814, Springer Verlag, 1994.

    Google Scholar 

  13. Z. Luo, R. Pollack, LEGO proof development system: user's manual, Technical Report, University of Edinburgh, 1992.

    Google Scholar 

  14. A. Massol, Presentation de Preuves en Langue Naturelle pour le Systéme Coq, Rapport de DEA, Universite de Nice-Sophia-Antipolis, 1993.

    Google Scholar 

  15. A. Ranta, Type Theory and the Informal Language of Mathematics, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.

    Google Scholar 

  16. L. Théry, Une methode distribuée de création d'interfaces et ses applications aux démonstrateurs de theoremes, PhD, Universite Denis Diderot, Paris, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia Antipolis, France

    Yann Coscoy, Gilles Kahn & Laurent Théry

Authors
  1. Yann Coscoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gilles Kahn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mariangiola Dezani-Ciancaglini Gordon Plotkin

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coscoy, Y., Kahn, G., Théry, L. (1995). Extracting text from proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014048

Download citation

  • DOI: https://doi.org/10.1007/BFb0014048

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59048-4

  • Online ISBN: 978-3-540-49178-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation