# * 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.