Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus
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 reas...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Springer
2002
|
| Online Access: | https://eprints.nottingham.ac.uk/322/ |
| _version_ | 1848790392637489152 |
|---|---|
| author | Zimmer, Juergen Dennis, Louise Abigail |
| author2 | Calmet, J. |
| author_facet | Calmet, J. Zimmer, Juergen Dennis, Louise Abigail |
| author_sort | Zimmer, Juergen |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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 osftware bus. We described the integration of the lambda-clam systems, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, lambda-clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, lambda-clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experimnents on proving theorems by induction using the computational power of the MAPLE system within lambda-clam. |
| first_indexed | 2025-11-14T18:11:53Z |
| format | Conference or Workshop Item |
| id | nottingham-322 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:53Z |
| publishDate | 2002 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3222020-05-04T20:32:29Z https://eprints.nottingham.ac.uk/322/ Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus Zimmer, Juergen Dennis, Louise Abigail 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 osftware bus. We described the integration of the lambda-clam systems, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, lambda-clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, lambda-clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experimnents on proving theorems by induction using the computational power of the MAPLE system within lambda-clam. Springer Calmet, J. Belaid, B. Capriotti, O. Hencoque, L. Sorge, Volker 2002 Conference or Workshop Item PeerReviewed Zimmer, Juergen and Dennis, Louise Abigail (2002) Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus. In: Artificial Intelligence, Automated Reasoning and Symbolic Computation (Calculemus 02), 2002, Marseille, France. |
| spellingShingle | Zimmer, Juergen Dennis, Louise Abigail Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title | Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title_full | Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title_fullStr | Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title_full_unstemmed | Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title_short | Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus |
| title_sort | inductive theorem proving and computer algebra in the mathweb software bus |
| url | https://eprints.nottingham.ac.uk/322/ |