Abstract:

Using Theory Morphisms for Implementing Formal Methods Tools

Achim D. Brucker and Burkhart Wolff


Tools for a specification language can be implemented directly (by building a special purpose theorem prover) 
or by a conservative embedding into a typed meta-logic, which allows their safe and logically consistent 
implementation and the reuse of existing theorem prover engines. For being useful, the conservative extension 
approach must provide derivations for several thousand ``folklore'' theorems.

In this paper, we present an approach for deriving the mass of these theorems mechanically from an existing 
library of the meta-logic. The approach presupposes a structured theory morphism mapping library datatypes 
and library functions to new functions of the specification language while uniformly modifying some semantic 
properties; for example, new functions may have a different treatment of undefinedness compared to old ones.