Skip to main content
SpringerLink
Log in

Critical Agents Supporting Interactive Theorem Proving

  • Conference paper
  • First Online:
Book cover Progress in Artificial Intelligence (EPIA 1999)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1695))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.B. Andrews. An Introduction To Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, San Diego, CA, USA, 1986.

    MATH  Google Scholar 

  2. 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.

    Article  MATH  MathSciNet  Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Chapter  Google Scholar 

  5. 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.

    Chapter  Google Scholar 

  6. 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.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. J. Denzinger D. Fuchs. Knowledge-Based Cooperation between Theorem Provers by TECHS. Seki Report SR-97-11, Fachbereich Informatik, Universität Kaiserslautern, 1997.

    Google Scholar 

  10. 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.

    Google Scholar 

  11. M. Fisher and A. Ireland. Multi-Agent Proof-Planning. In Workshop on Using AI Methods in Deduction at CADE-15, July 6–9 1998.

    Google Scholar 

  12. G. Gentzen. Untersuchungen über das Logische Schließen I und II. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.

    Article  MathSciNet  Google Scholar 

  13. 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.

    Google Scholar 

  14. 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.

    MATH  Google Scholar 

  15. M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, Cambridge, United Kingdom, 1993.

    MATH  Google Scholar 

  16. C.G. Jung. Experimenting with Layered, Resource-Adapting Agents in the Robocup Simulation. In Proceedings of the ROBOCUP’98 Workshop, 1998.

    Google Scholar 

  17. 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.

    Article  Google Scholar 

  18. 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.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. H.A. Simon. Models of Bounded Rationality. MIT Press, Cambridge, 1982.

    Google Scholar 

  21. S. Zilberstein. Models of Bounded Rationality. In AAAI Fall Symposium on Rational Agency, Cambridge, Massachusetts, November 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität des Saarlandes, D-66123, Saarbrücken, Germany

    Christoph Benzmüller & Volker Sorge

Authors
  1. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Volker Sorge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática, Universidade Nova de Lisboa, Quinta da Torre, P-2825-114, Caparica, Portugal

    Pedro Barahona

  2. Departamento de Matemática, Universidade de Évora, R. Romão Ramalho 59, P-7000, Évora, Portugal

    José J. Alferes

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation