Planning Proof Content for Communicating Induction

unofficial copies [PDF], [PS]

by Amanda M. Holland-Minkley

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


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.