System Name
B2Z list of NLG systems
System Builders Fiedler, Huang
Development Dates 1996-2000
Languages English
URL (if available)
who's who

Builds on: TAG-GEN


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.


Xiaorong Huang and Armin Fiedler.
Paraphrasing and aggregrating argumentative text using text structure.
In Proceedings of the 8th. International Workshop on Natural Language Generation (INLG '96), pages 21--30. Herstmonceux, England, June 1996. Main reference

X. Huang and A. Fiedler.
Proof verbalization as an application of NLG.
In IJCAI, pages 965--970, Nagoya, 1997.

Information last updated: 28.04.2002 (
Page last generated: 25-1-2009 21:01:38