Model building with ordered resolution: extracting models from saturated clause sets

A method is proposed to transform automatically some satisfiable clause sets S into clause sets S′ having a unique Herbrand model (w.r.t. a given signature) which also satisfies S. These clause sets with only one model can be used as representations of (in general infinite) Herbrand models of the initial set of clauses. Existing theorem provers may be used to evaluate literals and clauses in the models thus represented (using the standard proof by consistency mechanism). We also prove that for some classes of clauses, the extracted model can also be represented by a tree automaton on tuples of finite trees. This entails in particular that the evaluation of arbitrary function-free formulae in the represented models is decidable.