1999 Presentations (Communicative Events)
Verbalization of high-level formal proofs
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.
Subjects
Files
- holland-minkley_al_99.pdf application/pdf 113 KB Download File
More About This Work
- Academic Units
- Computer Science
- Publisher
- Proceedings of AAAI'99
- Published Here
- May 3, 2013