A method to combine algebraic computations with related deductions

Wolfgang Gehrke

Date: July 17th (Wednesday)
Time: ??.??
Abstract
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.

______________
__________________________________________

Previous page RISC SWP Linz Austria