Verbalization of High-Level Formal Proofs

unofficial copies [PDF], [PS]

by Amanda M. Holland-Minkley, Regina Barzilay, and Robert L. Constable

Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277-284, 1999.


We propose a new approach to text generation from formal proofs that exploits the high-level and interactive features of a tactic-style theorem prover. The design of our system is based on communication conventions identified in a corpus of texts. We show how to use dialogue with the theorem prover to obtain information that is required for communication but is not explicitly used in reasoning.