Tags:First-order, Refutationally complete, Saturation, Superposition and Unification
Abstract:
Classically, in saturation based proof systems, unification has been considered as a sub-procedure that can be used to restrict inferences. However, it is also possible to move unification to the calculus level, making the unification rules inferences themselves. For calculi that rely on unification procedures that return large or even infinite sets of unifiers, integrating unification into the calculus may be an attractive method of dovetailing between carrying out unification and carrying out inferences. This applies, for example, to AC-superposition and higher-order superposition. In this paper, we show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.