English summaries of mathematical proofs

Marianthi Alexoudi, Claus Zinn, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Automated theorem proving is becoming more important as the volume of applications in industrial and practical research areas increases. Due to the formalism of theorem provers and the massive amount of information included in machine-oriented proofs, formal proofs are difficult to understand without specific training. A verbalisation system, ClamNL, was developed to generate English text from formal representations of inductive proofs, as produced by the Clam proof planner. The aim was to generate natural language proofs that resemble the presentation of proofs found in mathematical textbooks and that contain only the mathematically interesting parts of the proof.
Original languageEnglish
Title of host publicationThe IJCAR 2004 Workshop on Computer-Supported Mathematical Theory Development
Number of pages12
Publication statusPublished - 2004


Dive into the research topics of 'English summaries of mathematical proofs'. Together they form a unique fingerprint.

Cite this