Extracting text from proofs

DOI10.1007/BFB0014048MaRDI QIDQ3024829zbMATH OpenFDO

Authors Yann Coscoy, G. Kahn, Laurent Théry

Publication date 4 July 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0014048

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• A natural language explanation for formal proofs
• scientific article; zbMATH DE number 4074537
• Presenting machine-found proofs
• scientific article; zbMATH DE number 1140678
• scientific article; zbMATH DE number 4164180

Cited in

(7)

• Declarative representation of proof terms
• Validation of proofs using PhoX
• Extracting Information from Logical Proofs
• A natural language explanation for formal proofs
• Context-relative syntactic categories and the formalization of mathematical text
• Translating between language and logic: what is easy and what is difficult
• ProofLang: the language of arXiv proofs

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Extracting text from proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3024829)