Abstract
We introduce a resource adaptive agent mechanism which supports the user of an interactive theorem proving system. The mechanism, an extension of [5], uses a two layered architecture of agent societies to suggest applicable commands together with appropriate command argument instantiations. Experiments with this approach show that its effectiveness can be further improved by introducing a resource concept. In this paper we provide an abstract view on the overall mechanism, motivate the necessity of an appropriate resource concept and discuss its realization within the agent architecture.
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
P.B. Andrews. An Introduction To Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, San Diego, CA, USA, 1986.
P.B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. Tps: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning, 16(3):321–353, 1996.
C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. ΩMega: Towards a Mathematical Assistant. In W. McCune, editor, Proceedings of the 14th Conference on Automated Deduction (CADE-14), LNAI, Townsville, Australia, 1997. Springer Verlag, Berlin, Germany.
C. Benzmüller and M. Kohlhase. LEO — a Higher-Order Theorem Prover. In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI, pages 139–144, Lindau, Germany, 1998. Springer.
C. Benzmüller and V. Sorge. A Blackboard Architecture for Guiding Interactive Proofs. In F. Giunchiglia, editor, Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the of the 8th International Conference AIMSA’98, number 1480 in LNAI, pages 102–114, Sozopol, Bulgaria, October 1998. Springer Verlag, Berlin, Germany.
C. Benzmüller and V. Sorge. Towards Fine-Grained Proof Planning with Critical Agents. In M. Kerber, editor, Informal Proceedings of the Sixth Workshop on Automated Reasoning Bridging the Gap between Theory and Practice in conjunction with AISB’99 Convention, pages 20–22, Edinburgh, Scotland, 8–9 April 1999. extended abstract.
A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction (CADE-9), volume 310 of LNCS, Argonne, IL, USA, 1988. Springer Verlag, Berlin, Germany.
J. Denzinger and I. Dahn. Cooperating Theorem Provers. In W. Bibel and P. Schmitt, editors, Automated Deduction — A Basis for Applications, volume 2, pages 483–416. Kluwer, 1998.
J. Denzinger D. Fuchs. Knowledge-Based Cooperation between Theorem Provers by TECHS. Seki Report SR-97-11, Fachbereich Informatik, Universität Kaiserslautern, 1997.
M. Fisher. An Open Approach to Concurrent Theorem Proving. In J. Geller, H. Kitano, and C. Suttner, editors, Parallel Processing for Artificial Intelligence, volume 3. Elsevier/North Holland, 1997.
M. Fisher and A. Ireland. Multi-Agent Proof-Planning. In Workshop on Using AI Methods in Deduction at CADE-15, July 6–9 1998.
G. Gentzen. Untersuchungen über das Logische Schließen I und II. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.
C. Gerber and C.G. Jung. Resource Management for Boundedly Optimal Agent Societies. In Proceedings of the ECAI’98 Workshop on Monitoring and Control of Real-Time Intelligent Systems, pages 23–28, 1998.
M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of LNCS. Springer Verlag, Berlin, Germany, 1979.
M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, Cambridge, United Kingdom, 1993.
C.G. Jung. Experimenting with Layered, Resource-Adapting Agents in the Robocup Simulation. In Proceedings of the ROBOCUP’98 Workshop, 1998.
W. McCune and L. Wos. Otter CADE-13 Competition Incarnations. Journal of Automated Reasoning, 18(2):211–220, 1997. Special Issue on the CADE-13 Automated Theorem Proving System Competition.
S.C. Shapiro. Compiling Deduction Rules from a Semantic Network into a Set of Process. In Abstracts of Workshop on Automated Deduction, Cambridge, MA, USA, 1977. MIT. Abstract only.
J. Siekmann, S. M. Hess, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, M. Kohlhase, K. Konrad, E. Melis, A. Meier, and V. Sorge. LΩUI: A Distributed Graphical User Interface for the Interactive Proof System ΩMEGA. Submitted to the International Workshop on User Interfaces for Theorem Provers, 1998.
H.A. Simon. Models of Bounded Rationality. MIT Press, Cambridge, 1982.
S. Zilberstein. Models of Bounded Rationality. In AAAI Fall Symposium on Rational Agency, Cambridge, Massachusetts, November 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benzmüller, C., Sorge, V. (1999). Critical Agents Supporting Interactive Theorem Proving. In: Barahona, P., Alferes, J.J. (eds) Progress in Artificial Intelligence. EPIA 1999. Lecture Notes in Computer Science(), vol 1695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48159-1_15
Download citation
DOI: https://doi.org/10.1007/3-540-48159-1_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66548-9
Online ISBN: 978-3-540-48159-1
eBook Packages: Springer Book Archive