# Superposition with Delayed Unification

arXiv: https://arxiv.org/abs/2403.04775 · HTML: https://mlsanity.com/paper/2403.04775/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 26 references that are in the map.
- First posted on arXiv 29 Feb 2024.

## Builds on (most cited first, 2 of 2)

- [Superposition for Lambda-Free Higher-Order Logic](https://mlsanity.com/paper/2005.02094/) (2020)
- [Superposition with Lambdas](https://mlsanity.com/paper/2102.00453/) (2021)

## Abstract (arXiv)

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.