System Name
B2Z list of NLG systems
System Builders Fiedler
Development Dates 2000-ongoing
Languages English
URL (if available)
who's who



P.rex is an interactive proof explanation system that adapts its explanations to the user and flexibly reacts to his questions or requests.


As a generic system, P.rex can be connected to different theorem provers, namely by means of the formal language TWEGA for specifying proofs and mathematical theories. Mathematical theories are organized in a hierarchical knowledge base. Each theory in it may contain, for example, axioms, definitions, and theorems along with proofs. A proof of a theorem can be represented hierarchically in TWEGA such that the various levels of abstraction are made explicit.

The central component of the system is the dialog planner. It is implemented in ACT-R, a goal-directed production system that aims to model human cognition. In ACT-R, declarative and procedural representations of knowledge are explicitly separated into the declarative memory and the procedural production rule base. The plan operators of the dialog planner are defined in terms of productions and the discourse plan is represented in the declarative memory.

The dialog plan is passed on through the sentence planner to the surface realizer. Currently, we use a derivate of PROVERB's sentence planner to plan the internal structure of the sentences, which are then realized by the surface realizer TAG-GEN.

The uttered sentences are finally displayed on the user interface. It also allows the user to enter remarks, requests and questions anytime. An analyzer receives the user's interactions and passes them on to the dialog planner. In the current stage, we use a simplistic analyzer that understands a small set of predefined interactions.


Main reference

Armin Fiedler.
Dialog-driven Adaptation to Explanations of Proofs.
In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), pages 1296--1300, Seattle, WA, 2001. Morgan Kaufmann.

Armin Fiedler.
P.rex: An Interactive Proof Explainer.
In Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR), pages 416--420. Springer-Verlag, 2001.

Armin Fiedler.
User-adaptive proof explanation.
PhD thesis, Naturwissenschaftlich-Technische Fakultät I, Universität des Saarlandes, Saarbrücken, Germany, 2001.

Armin Fiedler.
Using a cognitive architecture to plan dialogs for the adaptive explanation of proofs.
In 16th. International Joint Conference on Artificial Intelligence (IJCAI'99), pages 358--363, 1999.

Information last updated: 28.04.2002 (
Page last generated: 25-1-2009 21:01:38