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.
Preview
Unable to display preview. Download preview PDF.
References
L. Magnusson, B. Nordström, The ALF proof editor and Us proof engine, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.
D. Chester, The translation of Formal Proofs into English, Artificial Intelligence 7 (1976), 261–278, 1976.
A. Cohn, Proof Accounts in HOL, unpublished draft.
Y. Coscoy, Traductions de preuves en langage naturel pour le systeme Coq, Rapport de Stage, Ecole Polytechnique, 1994.
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.
Y. Bertot, the CtCoq Interface, available by ftp at babar.inria.fr: /pub/centaur/ctcoq.
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.
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.
A. Felty, Proof explanation and revision, Technical Report, University of Pennsylvania MS-CIS-88-17, 1988.
G. Gentzen, Investigations into logical deduction, in “The collected papers of Gerhard Gentzen”, M.E. Szabo (Ed.), pp. 69–131, North Holland, 1969.
M.J.C. Gordon, T.F. Melham, HOL: a proof generating system for higher-order logic, Cambridge University Press, 1992.
X. Huang, Reconstructing Proofs at the Assertion Level, in Proceedings of CADE-12, Nancy, LNAI 814, Springer Verlag, 1994.
Z. Luo, R. Pollack, LEGO proof development system: user's manual, Technical Report, University of Edinburgh, 1992.
A. Massol, Presentation de Preuves en Langue Naturelle pour le Systéme Coq, Rapport de DEA, Universite de Nice-Sophia-Antipolis, 1993.
A. Ranta, Type Theory and the Informal Language of Mathematics, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.
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.
Author information
Authors and Affiliations
Editor information
Rights 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