\begin{center}
\LARGE
A method to combine algebraic computations with related
                           deductions
\end{center}

\begin{center}
\Large
Wolfgang Gehrke
\end{center}

\noindent
Date:  July 17th (Wednesday)\\
Time:  14:50-15:15\\

\begin{center}
\large
Abstract
\end{center}

Several recent efforts focus on a practical combination of Computer Algebra Systems and
Automated Theorem Provers. Attempts were undertaken from either side to benefit from the
strengths of the other. We propose yet another approach which comes rather close to program
verification. 

Our method relies on a parametric representation of an algebraic notion. One instantiation by a
concrete operational structure as parameter results in an executable instance of the algebraic
notion. A further instantiation by a symbolic parameter provides a way for proving properties of
the new symbolic instance based on the properties of the given one. 

We illustrate this method by examples taken from the implementation of various number systems
in SML. The symbolic structures are completed by various semantic proof methods which allow to
prove or disprove restricted classes of formulae. All provided methods are decidable, i.e. work
automatically. We propose this case study as a possible benchmark for other approaches. 

