A method for simultaneous search for refutations and models by equational constraint solving (Q1198235)

A method for simultaneous search for refutations and Herbrand models is proposed. This problem is very interesting when the resolution procedure is used as a decision algorithm and when it is necessary to build a model for a satisfiable formula. New inference rules are proposed which are used in addition to a resolution rule. These new rules use distautology, dissubsumption, disresolution conditions which are formulated as formulas consisting of equalities and inequalities of terms. Introducing new rules it is possible to construct a resolution based decision algorithm for some classes of first order logic e.g. for the Bernays-Schönfinkel class for which no resolution methods is known to be a decision procedure.