From NLG Systems Wiki

Jump to: navigation, search



PROVERB is a system presenting machine-found proofs in natural language. It is embedded in the interactive proof development environment OMEGA. Settled between automated theorem proving (ATP) and natural language generation (NLG), PROVERB uses techniques of both these fields. In order to present proofs in a way as they can be found in mathematical textbooks, PROVERB first transforms and abstracts resolution proofs or natural deduction proofs to so-called assertion level proofs, which abstract from the basic calculus inference rules. Here, most justifications are in terms of the application of a definition, a lemma, or a theorem, which are collectively called assertions. Assertion level proofs are then verbalized in English using NLG techniques. First, a macroplanner determines the order and content of the information to be conveyed. Then, a microplanner plans the internal structure of the paragraphs and sentences. Finally, the surface sentences are produced by the system TAG-GEN. Furthermore, PROVERB allows for the automatic creation of a LaTeX document from the English proof.


  1. Huang, X., & Fiedler, A. (1997). Proof verbalization as an application of NLG. Paper presented at IJCAI, Nagoya. Bib
  2. Huang, X., & Fiedler, A. 1996. Paraphrasing and aggregrating argumentative text using text structure. Bib
Facts about PROVERBRDF feed
Descriptionnatural language presention of machine-found proofs  +
Domainformal proofs  +
Ended2000  +
ForerunnerTAG-GEN  +
LanguageEnglish  +
Started1996  +
URL  +
WorkerFiedler  +, and Huang  +
Personal tools