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

Architecture

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.