Skip to main content
PRL Project

Verbalization of High-Level Formal Proofs

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

Proceedings of Sixteenth National Conference on Artificial Intelligence

  • unofficial copies PDF, PS

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.

bibTex ref: HBC99

cite link