System Name 
PROVERB


System Builders  Fiedler, Huang


Development Dates  19962000  
Languages  English  
URL (if available)  http://www.ags.unisb.de/~afiedler/ 
PROVERB is a system presenting machinefound 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 socalled 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 TAGGEN. Furthermore, PROVERB allows for the automatic creation of a LaTeX document from the English proof. 
Information last updated: 28.04.2002 (dd.mm.yy)
Page last generated: 2512009 21:01:38