PROVERB
From NLG Systems Wiki
Summary
- System Name: PROVERB
- Short Description: natural language presention of machine-found proofs
- URL: http://www.ags.uni-sb.de/~afiedler/
- System Builders: Fiedler, Huang[1][2]
- Development Period: 1996–2000
- Languages: English
- Domain: formal proofs
- Forerunner: TAG-GEN
- Successors: P.rex
Description
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.
