Verbalization of high-level formal proofs
Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable · 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.