Inductive Theorem Proving and Computer Algebra in the MathWeb Software Bus

  • Jürgen Zimmer
  • Louise A. Dennis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


Reasoning systems have reached a high degree of maturity in the last decade. However, even the most successful systems are usually not general purpose problem solvers but are typically specialised on problems in a certain domain. The MathWeb Software Bus (MathWeb-SB) is a system for combining reasoning specialists via a common software bus. We describe the integration of the λ-Clam system, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, λ-Clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, λ-Clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experiments on proving theorems by induction using the computational power of the Maple system within λ-Clam.


Theorem Prove Computer Algebra Computer Algebra System Reasoning System Inductive Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AZ00]
    A. Armando and D. Zini. Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture. In A. Poggi, editor, Proceedings of the AI*IA-TABOO Joint Workshop ‘From Objects to Agents: Evolutionary Trends of Software Systems’, Parma, Italy, May 2000.Google Scholar
  2. [BCF+97]_C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, K. Kohlhase, A. Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge.Ωmega: Towards a mathematical assistant. In W. McCune, editor, Proc. of the 14th Conference on Automated Deduction, volume 1249 of LNAI, pages 252–255. Springer Verlag, 1997.Google Scholar
  3. [BCZ98]
    A. Bauer, E. Clarke, and X. Zhao. Analytica — an Experiment in Combining Theorem Proving and Symbolic Computation. Journal of Automated Reasoning (JAR), 21(3):295–325, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [BSvH+93]_A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. AI, 62:185–253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.zbMATHGoogle Scholar
  5. [BvHHS90]
    A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. InM. E. Stickel, editor, Proc. of the 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. LNAI No. 449. Also available from Edinburgh as DAI Research Paper 507.Google Scholar
  6. [CC98]
    O. Caprotti and A. M. Cohen. Draft of the Open Math standard. The Open Math Society, ects/OpenMath/omstd/, 1998.
  7. [Con]
    The Mozart Consortium. The mozart programming system.
  8. [CZ92]
    E. Clarke and X. Zhao. Analytica-A Theorem Prover for Mathematica. Technical Report CMU//CS-92-117, Carnegie Mellon University, School of Computer Science, October 1992.Google Scholar
  9. [DCN+00]_L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The prosper toolkit. In Proc. of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS-2000, LNCS, Berlin, Germany, 2000. Springer Verlag.Google Scholar
  10. [DGKM01]
    M. Dunstan, H. Gottliebsen, T. Kelsey, and U. Martin. A maple-pvs interface. Proc. of the Calculemus Symposium 2001, 2001.Google Scholar
  11. [FK99]
    A. Franke and M. Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Harald Ganzinger, editor, Proc. of the 16th Conference on Automated Deduction, volume 1632 of LNAI, pages 217–221. Springer Verlag, 1999.Google Scholar
  12. [HT93]
    J. Harrison and L. Théry. Extending the HOL Theorem Prover with a Computer Algebra System to Reason About the Reals. In C.-J. H. Seger J. J. Joyce, editor, Higher Order Logic Theorem Proving and its Applications (HUG’ 93), volume 780 of LNCS, pages 174–184. Springer Verlag, 1993.Google Scholar
  13. [IB96]
    A. Ireland and A. Bundy. Productive use of failure in inductive proof. JAR, 16(1-2):79–111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.zbMATHCrossRefMathSciNetGoogle Scholar
  14. [KKS96]
    M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra with Proof Planning. In Jaques Calmet and Carla Limongelli, editors, Design and Implementation of Symbolic Computation Systems; International Symposium, DISCO’ 96, Karlsruhe, Germany, September 18–20, 1996; Proc., volume 1128 of LNCS. Springer Verlag, 1996.Google Scholar
  15. [Koh00]
    M. Kohlhase. OMDoc: An open markup format for mathematical documents. Seki Report SR-00-02, Fachbereich Informatik, Universität des Saarlandes, 2000.
  16. [MFS02]
    E. Maclean, J. Fleuriot, and A. Smaill. Proof-planning non-standard analysis. In Proc. of the 7th International Symposium on Artificial Intelligence and Mathematics, 2002.Google Scholar
  17. [RS01]
    J. Richardson and A. Smaill. Continuations of proof strategies. In Maria Paola Bonacina and Bernhard Gramlich, editors, Proc. of the 4th International Workshop on Strategies in Automated Deduction, Siena, Italy, June 2001.Google Scholar
  18. [RSG98]
    J.D.C. Richardson, A. Smaill, and I. Green. System description: Proof planning in higher-order logic with lambda-clam. In C. Kirchner and H. Kirchner, editors, Proc. of the 15th International Conference on Automated Deduction, volume 1421 of LNCS, pages 129–133. Springer-Verlag, 1998.CrossRefGoogle Scholar
  19. [SG96]
    A. Smaill and I. Green. Higher-order annotated terms for proof search. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1275 of LNCS, pages 399–414, Turku, Finland, 1996. Springer-Verlag. Also available as DAI Research Paper 799.Google Scholar
  20. [Smo95]
    G. Smolka. The Oz programming model. In Jan van Leeuwen, editor, Computer Science Today, volume 1000 of LNCS, pages 324–343. Springer-Verlag, Berlin, 1995.CrossRefGoogle Scholar
  21. [Wal00]
    T. Walsh. Proof Planning in Maple. In Proc. of the CADE-17 workshop on Automated Deduction in the Context of Mathematics, 2000.Google Scholar
  22. [WNB92]
    T. Walsh, A. Nunes, and A. Bundy. The use of proof plans to sum series. In D. Kapur, editor, Proc. of the 11th Conference on Automated Deduction, volume 607 of LNCS, pages 325–339, Saratoga Spings, NY, USA, 1992. Springer Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jürgen Zimmer
    • 1
  • Louise A. Dennis
    • 2
  1. 1.Division of InformaticsUniversity of EdinburghUK
  2. 2.School of Computer Science and Information TechnologyUniversity of NottinghamThe Netherlands

Personalised recommendations