# Computing Finite Models by Reduction to Function-Free Clause Logic

Peter Baumgartner,
Alexander Fuchs,
Hans de Nivelle,
and Cesare
Tinelli
### 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.

Alexander Fuchs
Last modified: Thu Apr 26 09:46:07 CDT 2007