@Article{Baumgartner:etal:MEFiniteModels:JAL:2007,
  author = {Peter Baumgartner and Alexander Fuchs and Hans de Nivelle and Cesare Tinelli},
  title = {Computing Finite Models by Reduction to Function-Free Clause Logic},
  year = {2007},
  series        = {{J}ournal of {A}pplied {L}ogic},
  publisher = {Elsevier},
  abstract = {
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 
because 
the propositional formulas to be considered may become very large. 

We propose instead to reduce model search to a sequence 
of satisfiability problems consisting 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 this paper we describe our proposed reduction in detail
and discuss how it is integrated into the Darwin prover,
our implementation of the Model Evolution calculus.
The results are general, however, as our approach can be 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.
},
}