Blocking and Other Enhancements for Bottom-Up Model Generation Methods

Baumgartner, P. and Schmidt, R. A. (2006)

In Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139. BiBTeX, Full text via Springer.

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.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 10 Oct 06
Copyright © 2006 Renate A. Schmidt, School of Computer Science, Man Univ,