Superposition with Delayed Unification
This addresses a technical bottleneck in automated theorem proving for researchers in formal verification and logic, though it appears incremental.
The paper tackles the problem of integrating unification into saturation-based proof systems by moving unification rules to the calculus level, showing that first-order superposition remains complete with this approach and providing experimental evaluation.
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.