Abstract

If Σ is a set of symbols, a formula F is said to be non-ambiguous if all models of F coincide on the terms built on Σ . Non-ambiguous formulae can be used as representations of a Herbrand interpretation defined on the signature Σ. An important advantage of this technique is that any existing theorem prover may be used to evaluate literals and clauses in the models thus represented .In this work, a method is proposed to extract automatically from some satisfiable clause sets S a non ambiguous formula F such that the interpretation represented by F is a model of S. In contrast to previous works, clauses occurring in S may contain equational literals and can have more than one maximal literal