  Model generation is a problem complementary to theorem proving and is
important for fault analysis and debugging of formal specifications of security
protocols, programs and terminological definitions. This paper discusses
several ways of enhancing the paradigm of bottom-up model generation. The two
main contributions are new, generalized blocking techniques and a new
range-restriction transformation. The blocking techniques are based on simple
transformations of the input set together with standard equality reasoning and
redundancy elimination techniques. These provide general methods for finding
small, finite models. The range-restriction transformation refines existing
transformations to range-restricted clauses by carefully limiting the creation
of domain terms. All possible combinations of the introduced techniques and
classical range-restriction were tested on the clausal problems of the TPTP
Version 6.0.0 with an implementation based on the SPASS theorem prover using a
hyperresolution-like refinement. Unrestricted domain blocking gave best results
for satisfiable problems showing it is a powerful technique indispensable for
bottom-up model generation methods. Both in combination with the new
range-restricting transformation, and the classical range-restricting
transformation, good results have been obtained. Limiting the creation of terms
during the inference process by using the new range restricting transformation
has paid off, especially when using it together with a shifting transformation.
The experimental results also show that classical range restriction with
unrestricted blocking provides a useful complementary method. Overall, the
results showed bottom-up model generation methods were good for disproving
theorems and generating models for satisfiable problems, but less efficient
than SPASS in auto mode for unsatisfiable problems.
