Skip to main content
PRL Project

Planning Proof Content for Communicating Induction

by Amanda Holland-Minkley

Proceedings of Second International Natural Language Generation Conference, pp. 167-172

  • unofficial copies PDF, PS

We describe some of the complications involved in expressing the technique of induction when automatically generating textual versions of formal mathematical proofs produced by a theorem proving system, and describe our approach to this problem. The pervasiveness of induction within mathematical proofs makes its effective generation vital to readable proof texts. Our focus is on planning texts involving induction. Our efforts are driven by a corpus of human-produced proof texts, incorporating both regularities within this corpus and the formal structure of induction into coherent text plans.

bibTex ref: Hol02

cite link