A Basis for Model Computation in Free Data Types

Wolfgang Ahrendt


Abstract data types, specified by some equality logic under the
assumption of term generatedness, are called `free', if terms, built
only by constructors, are semantically unique. This paper presents a
calculus, intended to search for models of free data type
specifications.  A semantical view is discussed, where the uniqueness
of constructor terms is `hard wired'. This suggests an explicit
reasoning about interpretations instead of performing real equality
reasoning.  The rules, which depend on signature, constructor
definitions and axioms, are formulated as range restricted
clauses. This allows to `perform' the calculus simply by calling a
model generation prover, in particular the MGTP system.

This approach is a `basis' only, because one of the core problems in
model construction, the terminating detection of satisfying models, is
not yet solved for the described frame. Perspectives in this issue are
briefly discussed against the background of using the method for
disproving conjectures about consistent data types.