Abstract

It is shown that a combination of semantic resolution and ordered paramodulation provides a decision procedure for a large class PVD=g of clause sets with equality. It is also demonstrated how the inference system can be transformed into an algorithm that extracts finite descriptions of Herbrand models from sets of clauses. This algorithm always terminates on clause sets in PVD=g and yields an appropriate model representation. Moreover, an algorithm for evaluating arbitrary clauses over the represented models is defined. Finally, it is proved that PVD=g enjoys the finite model property and shown how finite models can be algorithmically extracted from model representations of this type