ML Anthology

Verbalization of High-Level Formal Proofs

Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable
AAAI 1999 pp. 277-284
doi:10.7916/d8k3630v /aaai/1999/hollandminkley1999aaai-verbalization/

Abstract

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.

PDF AAAI Semantic Scholar

Cite

Text

Holland-Minkley et al. "Verbalization of High-Level Formal Proofs." AAAI Conference on Artificial Intelligence, 1999. doi:10.7916/d8k3630v

Markdown

[Holland-Minkley et al. "Verbalization of High-Level Formal Proofs." AAAI Conference on Artificial Intelligence, 1999.](https://mlanthology.org/aaai/1999/hollandminkley1999aaai-verbalization/) doi:10.7916/d8k3630v

BibTeX

@inproceedings{hollandminkley1999aaai-verbalization,
  title     = {{Verbalization of High-Level Formal Proofs}},
  author    = {Holland-Minkley, Amanda M. and Barzilay, Regina and Constable, Robert L.},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {1999},
  pages     = {277-284},
  doi       = {10.7916/d8k3630v},
  url       = {https://mlanthology.org/aaai/1999/hollandminkley1999aaai-verbalization/}
}