Efficient model generation through compilation

We present a collection of simple but powerful techniques for enhancing the efficiency of tableau-based model generators such as Satchmo. The central ideas are to compile a clausal first order theory into a procedural Prolog program and to avoid redundant work of a naive implementation. We have comp ared various combinations of our techniques among each other and with theor em provers based on various calculi, using the TPTP problem library as a be nchmark. Our implementation has turned out to be the most efficient for ran ge-restricted problems and for a class of problems we call nonnesting. (C) 2000 Academic Press.