Abstract
This paper outlines the interactive proof explanation system P.rex , which adapts its explanation to the user and allows him anytime to utter questions or requests, to which it reacts flexibly. As a generic system, it can be connected to different theorem provers. The distribution is available via the P.rex home page at http://www.ags.uni-sb.de/~prex.
Acknowledgments
The author wishes to thank Frank Pfenning and Carsten Schürmann for their help in the development and the implementation of TWEGA and Christian Lebiere for his help in the use of ACT-R.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
John R. Anderson and Christian Lebiere. The Atomic Components of Thought. Lawrence Erlbaum, 1998.
C. Benzmüller, et al. Ωmega: Towards a mathematical assistant. In William McCune, ed., Proc. of the 14th Conference on Automated Deduction, number 1249 in LNAI, pages 252–255, Townsville, Australia, 1997. Springer Verlag.
Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, 1988.
Armin Fiedler. Using a cognitive architecture to plan dialogs for the adaptive explanation of proofs. In Thomas Dean, ed., Proc. of the 16th International Joint Conference on Artificial Intelligence (IJCAI), pages 358–363, Stockholm, Sweden, 1999. Morgan Kaufmann.
Armin Fiedler. Dialog-driven adaptation of explanations of proofs. In Proc. of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, Washington, 2001. In press.
Armin Fiedler. User adaptive proof explanation. PhD thesis, University of the Saarland, Saarbrücken, Germany, 2001. In preparation.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, 1993.
Xiaorong Huang and Armin Fiedler. Proof verbalization as an application of NLG. In Martha E. Pollack, ed., Proc. of the 15th International Joint Conference on Artificial Intelligence (IJCAI), pages 965–970, Nagoya, Japan, 1997. Morgan Kaufmann.
Anne Kilger and Wolfgang Finkler. Incremental generation for realtime applications. Research Report RR-95-11, DFKI, Saarbrücken, Germany, July 1995.
Frank Pfenning and Carsten Schürmann. System description: Twelf — a metalogical framework for deductive systems. In Harald Ganzinger, ed., Proc. of the 16th Conference on Automated Deduction, number 1632 in LNAI, pages 202–206. Springer Verlag, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fiedler, A. (2001). P.rex: An Interactive Proof Explainer. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_33
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive