@Unpublished{Baumgartner:etal:FiniteModels:2006,
  author = {Peter Baumgartner and Alexander Fuchs and Hans de Nivelle and Cesare Tinelli},
  title = {Computing Finite Models by Reduction to Function-Free Clause Logic},
  month = {June},
  year = {2006},
  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, 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.},
  url = {http://www.cs.uiowa.edu/~fuchs/PAPERS/darwin-FM.pdf},
  note = {to appear, preliminary version},
}