View Related Documents

Abstract

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.
The author is supported by the European Union IHP grant CALCULEMUS HPRN-CT-2000-00102.
The author was funded by EPSRC grant Gr/M45030.

Fulltext Preview

Image of the first page of the fulltext document