Edinburgh Research Explorer

English summaries of mathematical proofs

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

Related Edinburgh Organisations

Open Access permissions


Original languageEnglish
Title of host publicationThe IJCAR 2004 Workshop on Computer-Supported Mathematical Theory Development
Number of pages12
Publication statusPublished - 2004


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.

Download statistics

No data available

ID: 16426131