Skip to main content
SpringerLink
Log in

Experiments with an Agent-Oriented Reasoning System

  • Conference paper
  • First Online:
KI 2001: Advances in Artificial Intelligence (KI 2001)

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

Included in the following conference series:

Abstract

This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems

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.

Reference

  1. J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT:A system for distributed equational deduction. In Proc. of RTA-95, LNCS 914. Springer, 1995.

    Google Scholar 

  2. P. Andrews. General models, descriptions and choice in type theory. Journal of Symbolic Logic, 37(2):385–394, 1972.

    Article  MATH  MathSciNet  Google Scholar 

  3. A. Armando and D. Zini. nterfacing computer algebra and deduction systems via the logic broker architecture. In [CAL01].

    Google Scholar 

  4. C. Benzmüller et al. Omega: Towards a mathematical assistant. In Proc. of CADE-14, LNAI 1249. Springer, 1997.

    Google Scholar 

  5. C. Benzmüller, M. Jamnik, M. Kerber, and V. Sorge. Agent Based Mathematical Reasoning. In CALCULEMUS-99, Systems for Integrated Computation and Deduction, volume 23 (3) of ENTCS. Elsevier, 1999.

    Google Scholar 

  6. C. Benzmüller and M. Kohlhase. LEO-a higher-order theorem prover. In Proc. of CADE-15, LNAI 1421. Springer, 1998.

    Google Scholar 

  7. M. Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, in press, 2001.

    Google Scholar 

  8. C. Benzmüller and V. Sorge. Critical Agents Supporting Interactive Theorem Proving. Proc. of EPIA-99, LNAI 1695, Springer, 1999.

    Google Scholar 

  9. C. Benzmüller and V. Sorge. OANTS-An open approach at combining Interactive and Automated Theorem Proving. In [CAL01].

    Google Scholar 

  10. CALCULEMUS-2000, Systems for Integrated Computation and Deduction. AK Peters, 2001.

    Google Scholar 

  11. L. Cheikhrouhou and V. Sorge. PDS A Three-Dimensional Data Structure for Proof Plans. In Proc. of ACIDCA’2000, 2000.

    Google Scholar 

  12. I. Dahn and J. Denzinger. Cooperating theorem provers. In Automated Deduction-A Basis for Applications, volume II. Kluwer, 1998.

    Google Scholar 

  13. J. Denzinger and D. Fuchs. Cooperation of Heterogeneous Provers. In Proc. of IJCAI-99, 1999.

    Google Scholar 

  14. J. Denzinger and M. Kronenburg. Planning for distributed theorem proving: The teamwork approach. In Proc. of KI-96, LNAI 1137. Springer, 1996.

    Google Scholar 

  15. A. Franke, S. Hess, Ch. Jung, M. Kohlhase, and V. Sorge. Agent-Oriented Integration of Distributed Mathematical Services. Journal of Universal Computer Science, 5(3):156–187, 1999.

    MATH  Google Scholar 

  16. M. Fisher and A. Ireland. Multi-agent proof-planning. CADE-15Workshop “Using AI methods in Deduction”, 1998.

    Google Scholar 

  17. A. Fiedler. P.rex: An interactive proof explainer. In R. Goré, A. Leitsch, and T. Nipkow (eds), Automated Reasoning-Proceedings of the First International Joint Conference, IJCAR, LNAI 2083. Springer, 2001.

    Google Scholar 

  18. M. Fisher. An Open Approach to Concurrent Theorem Proving. In Parallel Processing for Artificial Intelligence, volume 3. Elsevier, 1997.

    Google Scholar 

  19. M. Fisher and M. Wooldridge. A Logical Approach to the Representation of Societies of Agents. In Artificial Societies. UCL Press, 1995.

    Google Scholar 

  20. A. Ireland and A. Bundy. Productive use of failure in inductive proof. Special Issue of the Journal of Automated Reasoning, 16(1-2):79–111, 1995.

    Article  MathSciNet  Google Scholar 

  21. A. Meier. Tramp-transformation of machine-found proofs into ND-proofs at the assertion level. In Proc. of CADE-17, LNAI 1831. Springer, 2000.

    Google Scholar 

  22. J. Müller. A Cooperation Model for Autonomous Agents. In Proc. of the ECAI’96 Workshop Intelligent Agents III, LNAI 1193. Springer, 1997.

    Google Scholar 

  23. H. Nii, E. Feigenbaum, J. Anton, and A. Rockmore. Signal-to-symbol transformation: HASP/SIAP case study. AIMagazine, 3(2):23–35, 1982.

    Google Scholar 

  24. J. Rice. The ELINT Application on Poligon: The Architecture and Performance of a Concurrent Blackboard System. In Proc. of IJCAI-89. Morgan Kaufmann, 1989.

    Google Scholar 

  25. J. Siekmann et al. Loui: Lovely Omega user interface. Formal Aspects of Computing, 11(3):326–342, 1999.

    Article  Google Scholar 

  26. G. Weiss, editor. Multiagent systems: a modern approach to distributed artificial intelligence. MIT Press, 1999.

    Google Scholar 

  27. A. Wolf. P-SETHEO: Strategy Parallelism in Automated Theorem Proving. In Proc. of TABLEAUX-98, LNAI 1397. Springer, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany

    Christoph Benzmüller & Volker Sorge

  2. School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK

    Manfred Kerber

Authors
  1. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manfred Kerber
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mateja Jamnik
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Volker Sorge
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany

    Franz Baader

  2. Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany

    Gerhard Brewka

  3. Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria

    Thomas Eiter

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benzmüller, C., Kerber, M., Jamnik, M., Sorge, V. (2001). Experiments with an Agent-Oriented Reasoning System. In: Baader, F., Brewka, G., Eiter, T. (eds) KI 2001: Advances in Artificial Intelligence. KI 2001. Lecture Notes in Computer Science(), vol 2174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45422-5_29

Download citation

  • DOI: https://doi.org/10.1007/3-540-45422-5_29

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42612-7

  • Online ISBN: 978-3-540-45422-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation