Superposition with Delayed Unification

TL;DR

This paper investigates integrating unification into the calculus by delaying unification and representing unresolved pairs as constraint literals, enabling a calculi-based dovetail with inference rules. It introduces a modified superposition calculus, Inf, which performs single-step unification and propagates subproblems as constraints, complemented by ground counterparts and a selection-driven framework to control complexity. The authors prove static and dynamic refutational completeness within Waldmann et al.'s framework and implement the approach in Vampire, alongside fingerprint-index variants and eager constraint solving. Experimental results show that delayed unification generally underperforms standard first-order unification in practice, but the method provides a principled template for extending completeness arguments to more complex unification (e.g., higher-order, unification modulo theories) and for exploring practical hybrids.

Abstract

Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. 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.