Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae (Q4795877)

The resolution method is a fundamental tool in automated deduction. However, an important difference of this method w.r.t. other theorem provers (i.e. tableau calculi) is that resolution does not provide a model of the formula when it is satisfiable. Several methods, in the context of resolution, have been proposed to extract such a model, although no general solution exists. In this paper, a method is designed for this purpose. This method is based on extracting clause sets that are saturated under some order refinements of the resolution rule to prune the search space. The author has published some previous results in this field, but they had several limitations. Most of them are overcome in the present paper. See, for example, \textit{N. Peltier}, ``Model building with ordered resolution: Extracting models from saturated clause sets'' [J. Symb. Comput. (to appear)].