非表示:
キーワード:
-
要旨:
We propose to reduce model search to a sequence of satisfiability
problems made of function-free clause sets, and to apply
efficient theorem provers capable of deciding such problems on
them.
The main motivation for this method is the fact that
first-order clause sets
grow more slowly than their propositional counterparts, thus
allowing for more space-efficient reasoning.
We describe the method in detail, and show how it is integrated
into Darwin, which is an implementation of the model evolution
calculus. Although we used Darwin, the results are general,
as our approach can be used
in principle with every system that decides the satisfiability
of function-free first-order clause sets.
