Superposition with Delayed Unification

Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson
2/29/2024
cs.LOcs.AI

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Anti-unification and Generalization: A Survey

83% match2023

SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

80% match2023

Higher-Order Pattern Unification Modulo Similarity Relations

73% match2025

Solver-Aided Expansion of Loops to Avoid Generate-and-Test

72% match2025

From Euler to AI: Unifying Formulas for Mathematical Constants

71% match1 repo42025

Translating SUMO-K to Higher-Order Set Theory

71% match2023

Cite this paper

@article{bhayat2024superposition,
  title  = {Superposition with Delayed Unification},
  author = {Ahmed Bhayat and Johannes Schoisswohl and Michael Rawson},
  year   = {2024},
  eprint = {2403.04775},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2403.04775v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2403.04775.svg)](https://codeofpaper.com/paper/2403.04775)

Discussion