Computing Finite Models by Reduction to Function-Free Clause Logic
Alexander Fuchs and Cesare
Recent years have seen considerable interest in procedures for computing finite
models of first-order logic specifications. One of the major paradigms,
MACE-style model building, is based on reducing model search to a sequence of
propositional satisfiability problems and applying (efficient) SAT solvers
to them. A problem with this method is that it does not scale well, as the
propositional formulas to be considered may become very large.
We propose instead to reduce model search to a sequence of satisfiability problems
made of function-free first-order clause sets, and to apply (efficient) theorem
provers capable of deciding such problems. The main appeal of this method is that
first-order clause sets grow more slowly than their propositional counterparts,
thus allowing for more space efficient reasoning.
In the paper we describe the method in detail and show how it is integrated into
one such prover, Darwin, our implementation of the Model Evolution calculus.
The results are general, however, as our approach can used in principle with any
system that decides the satisfiability of function-free first-order clause sets.
To demonstrate its practical feasibility, we tested our approach on all satisfiable
problems from the TPTP library. Our methods can solve a significant subset of these
problems, which overlaps but is not included in the subset of problems solvable by
state-of-the-art finite model builders such as Paradox and Mace4.},
Last modified: Fri Jun 9 03:31:41 CDT 2006