PRL Seminars 1998-99

We have been working on building a system that automatically generates English language versions of Nuprl proofs. We have developed a new approach to 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.

This is joint work with Regina Barzilay and Robert Constable.