Inductive Theorem Proving and Computer Algebra in the MathWeb Software Bus
- 218 Downloads
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.
KeywordsTheorem Prove Computer Algebra Computer Algebra System Reasoning System Inductive Proof
Unable to display preview. Download preview PDF.
- [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
- [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
- [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
- [CC98]O. Caprotti and A. M. Cohen. Draft of the Open Math standard. The Open Math Society, http://www.nag.co.uk/proj ects/OpenMath/omstd/, 1998.
- [Con]The Mozart Consortium. The mozart programming system. http://www.mozart-oz.org/.
- [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
- [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
- [DGKM01]M. Dunstan, H. Gottliebsen, T. Kelsey, and U. Martin. A maple-pvs interface. Proc. of the Calculemus Symposium 2001, 2001.Google Scholar
- [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
- [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
- [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
- [Koh00]M. Kohlhase. OMDoc: An open markup format for mathematical documents. Seki Report SR-00-02, Fachbereich Informatik, Universität des Saarlandes, 2000. http://www.mathweb.org/omdoc.
- [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
- [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
- [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
- [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
- [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
- [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