Computer algebra systems (CASs) and automated theorem provers (ATPs) exhibit complementary abilities. CASs focus on efficiently
solving domain-specific problems. ATPs are designed to allow for the formalization and solution of wide classes of problems
within some logical framework. Integrating CASs and ATPs allows for the solution of problems of a higher complexity than those
confronted by each class alone. However, most experiments conducted so far followed an ad-hoc approach, resulting in tailored
solutions to specific problems. A structured and principled approach is necessary to allow for the sound integration of systems
in a modular way. The Open Mechanized Reasoning Systems (OMRS) framework was introduced for the specification and implementation
of mechanized reasoning systems, e.g. ATPs. The approach was recasted to the domain of computer algebra systems. In this paper,
we introduce a generalization of OMRS, named OMSCS (Open Mechanized Symbolic Computation Systems). We show how OMSCS can be
used to soundly express CASs, ATPs, and their integration, by formalizing a combination between the Isabelle prover and the
Maple algebra system. We show how the integrated system solves a problem which could not be tackled by each single system
alone.
Topics Integration of Logical Reasoning and Computer Algebra - Computer Algebra Systems and Automated Theorem Provers
Keywords Computer Algebra Systems - Theorem Provers - Integration - Formal Frameworks