System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving

1. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321–353, 1996.

   Article  MATH  MathSciNet  Google Scholar 

2. 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. InWilliam McCune, editor, Proceedings of the 14th Conference on Automated Deduction, number 1249 in LNAI, pages 252–255, Townsville, Australia, 1997. Springer Verlag.

   Google Scholar 

3. Christoph Benzmüller and Michael Kohlhase. LEO-a higher order theorem prover. In Claude Kirchner and Hél*#x00E8;ne Kirchner, editors, Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI, pages 139–144, Lindau, Germany, 1998. Springer Verlag.

   Google Scholar 

4. The open math standard. Open Math Consortium, http://www.openmath.org, 1998.

5. T. Finin and R. Fritzson. KQML — a language and protocol for knowledge and information exchange. In Proceedings of the 13th Intl. Distributed Artificial Intelligence Workshop, pages 127–136, Seattle, WA, USA, 1994.

   Google Scholar 

6. Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, and Volker Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 1999. forthcoming. 8 Either by using MathWeb directly, or by cooperating with the authors.

   Google Scholar 

7. Xiaorong Huang and Armin Fiedler. Presenting machine-found proofs. In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th Conference on Automated Deduction, number 1104 in LNAI, pages 221–225, New Brunswick, NJ, USA, 1996. Springer Verlag.

   Google Scholar 

8. Manfred Kerber, Michael Kohlhase, and Volker Sorge. Integrating computer algebra into proof planning. Journal of Automated Reasoning, 21(3):327–355, 1998.

   Article  MATH  MathSciNet  Google Scholar 

9. Andreas Meier. Translation of automatically generated proofs at assertion level. Technical Report forthcoming, Universität des Saarlandes, 1999.

   Google Scholar 

10. Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, and Volker Sorge. A distributed graphical user interface for the interactive proof system OMEGA. In Roland C. Backhouse, editor, User Interfaces for Theorem Provers, number 98-08 in Computing Science Reports, pages 130–138, Department of Mathematics and Computing Science, Eindhoven Technical University, 1998.

    Google Scholar 

11. M. Kohlhase, S. Hess, Ch. Jung and V. Sorge. An implementation of distributed mathematical services. In 6th CALCULEMUS and TYPES Workshop, Eindhoven, The Netherlands, July 13–15 1998. Electronic Procedings: http://www.win.tue.nl/math/dw/pp/calc/proceedings.html.

    Google Scholar 

12. Jon Siegel. CORBA: Fundamentals and Programming. John Wiley & Sons, Inc., 1996.

    Google Scholar 

13. Geoff Sutcliffe and Christian Suttner. The cade-14 atp system competition. Journal of Automated Reasoning, 21(2):177–203, 1998.

    Article  MATH  MathSciNet  Google Scholar 

Download references