Model building by resolution

Abstract

Resolution calculi are best known as basis for algorithms testing the unsatisfiability of sets of clauses. Only recently more attention is paid to the fact that various resolution refinements may also benefitly be employed as decision procedures for a wide range of decidable classes of clause sets. In this proof theoretic approach to the decision problem one usually tries to test for satisfiability by termination of complete resolution procedures. Building on such types of decidability results we show that, for certain classes of clause sets, we can extract (representations of) models from the set of resolvents generated by hyperresolution. The process of model construction proceeds in two steps: First hyperresolution is employed to arrive at a finite set of atoms that represents a description of an Herbrand-model. In a second step we extract from this set of atoms a full representation of a model with finite domain. We emphasize that no backtracking is needed in our model constructing algorithm.