Academic Commons

Presentations (Communicative Events)

Verbalization of high-level formal proofs

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

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.

Files

More About This Work

Academic Units
Computer Science
Publisher
Proceedings of AAAI'99
Published Here
May 3, 2013
Academic Commons provides global access to research and scholarship produced at Columbia University, Barnard College, Teachers College, Union Theological Seminary and Jewish Theological Seminary. Academic Commons is managed by the Columbia University Libraries.