English Summaries of Mathematical Proofs
(\~2003)Аннотация
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.