Blocking and other enhancements for bottom-up model generation methods

In this paper we introduce several new improvements to the bottom-up model generation (BUMG) paradigm. Our techniques are based on non-trivial transformations of first-order problems into a certain implicational form, namely range-restricted clauses. These refine existing transformations to range-restricted form by extending the domain of interpretation with new Skolem terms in a more careful and deliberate way. Our transformations also extend BUMG with a blocking technique for detecting recurrence in models. Blocking is based on a conceptually rather simple encoding together with standard equality theorem proving and redundancy elimination techniques. This provides a general-purpose method for finding small models, The presented techniques are implemented and have been successfully tested with existing theorem provers on the satisfiable problems from the TPTP library. © Springer-Verlag Berlin Heidelberg 2006.