@INPROCEEDINGS{BaumgartnerSchmidt06,
AUTHOR = {Baumgartner, P. and Schmidt, R. A.},
YEAR = {2006},
TITLE = {Blocking and Other Enhancements for Bottom-Up Model Generation Methods},
EDITOR = {Furbach, U. and Shankar, N.},
BOOKTITLE = {Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {4130},
PUBLISHER = {Springer},
PAGES = {125--139},
URL = {http://www.cs.man.ac.uk/~schmidt/BaumgartnerSchmidt06.html}
ABSTRACT = {
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.
}
}