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.
Registration: ISBN 978-0-262-51106-3
Copyright: July 18-22, 1999, Orlando, Florida. Published by The AAAI Press, Menlo Park, California.