From NLG Systems Wiki

Jump to: navigation, search


[edit] Summary


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.


  1. Fiedler, A. (2001). Dialog-driven Adaptation to Explanations of Proofs. Paper presented at Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, WA. Bib
  2. Fiedler, A. (2001). P.rex: An Interactive Proof Explainer. Paper presented at Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR). Bib
  3. Fiedler, A. ((2001). User-adaptive proof explanation.). Unpublished PhD Thesis, Saarbrücken, Germany. Bib
  4. Fiedler, A. (1999). Using a cognitive architecture to plan dialogs for the adaptive explanation of proofs. Paper presented at 16th. International Joint Conference on Artificial Intelligence (IJCAI'99). Bib
Facts about P.rexRDF feed
Descriptionan interactive, user-adaptive proof explanation system  +
Domainproofs  +
ForerunnerPROVERB  +, and TAG-GEN  +
LanguageEnglish  +
NameP.rex  +
Started2000  +
URLhttp://www.ags.uni-sb.de/~prex  +
WorkerFiedler  +
Personal tools