Proof presentation in the Omega system
by Erica Melis
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.