KnowledgeBase » 
SEMINAR
» ID = 526
Proof presentation in the Omega system
by Erica Melis
1999-2000
Currently we have two proof presentations in Omega:
(1) the Proverb system that verbalizes proofs at the assertion-level, and,
(2) a verbalization of methods and proofs at the plan-level.
These two systems will be
integrated into a new Proverb soon which will present proofs at the plan-level and
other levels of detail and that will use hypertext facilities based on MAthML.
Proverb has been developed for verbalizing proofs found by traditional automated
theorems provers. It abstracts, say resolution proofs, to assertion level and uses
several NLG techniques to come up with a concise and readable proof. Proverb
consists of a macroplanner that decides what to verbalize, a microplanner that
computes how to verbalize, and a realizer that produces the actual text.
The plan-level verbalization doe not use elaborate linguistic techniques but
verbalizes methods schematically, based on the pretty schematic verbalizations found
in textbooks. Since we use hypertext here we can hide and unhide subproofs and
provide the hierarchical structure that is given by the proof plan. Empirical evidence
shows that these features are very important for proof understanding.