The presented approach aims at identifying false conjectures about
free data types. Given a specification and a conjecture, the method
performs a search for a model of an according counter
specification. The model search is tailor-made for the semantical
setting of free data types, where the fixed domain allows to describe
models just in terms of interpretations. For sake of
interpretation construction, a theory specific calculus is provided.
The concrete rules are `executed' by a procedure known as model
generation. As most free data types have infinite domains, the
ability of automatically solving the non-consequence problem is
necessarily limited. That problem is addressed by limiting the
instantiation of the axioms. This approximation leads to a
restricted notion of model correctness, which is discussed. At the
same time, it enables model completeness for free data types, unlike
approaches based on limiting the domain size.