Karsten Homann and Jacques Calmet Abstract
As an example for the development of a common environment for doing mathematics we implemented a prototype of an interface between the tactical theorem prover Isabelle and Maple. The interface is realized by extending the simplifier of Isabelle without any modification of Maple. Since we do not have to take into consideration any idiosyncrasies of Maple except its syntax, it would be very easy to link Isabelle to another CAS as well. The simplifier is extended by the introduction of a new class of simplification rules called evaluation rules in order to make selected operations of Maple available. Additionaly, we specify syntax translations for the concrete syntax of Maple. They enable Isabelle to communicate with the computer algebra system to solve a set of exemplary problems. Another prototype connects Magma and the theorem prover Dtp to compute and prove theorems in group theory.