A calculus combining resolution and enumeration for building finite models

A calculus is proposed for simultaneous search for refutations and models for sets of clauses. It combines existing resolution-based model building approaches with enumeration techniques that are usually restricted to tableau-based theorem provers or finite model builders. The method is sound, refutationally complete, and builds models for any satisfiable set of clauses having a finite model. It strictly enlarges the scope of resolution-based model building, by allowing one to build models for sets of clauses for which resolution does not terminate.