mlsanityData to 14 Oct 2026

Superposition with Lambdas

arXiv 2102.00453 ↗First posted 31 Jan 2021cs.LO cs.AIcited by 1

Not on the map. Why?

Abstract (arXiv)

We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on βη-equivalence classes of λ-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 5 of its 88 references that are in the map. First posted on arXiv 31 Jan 2021.

Builds on

5 of 88 references.

References · 5

  1. 2013HOL(y)Hammer: Online ATP Service for HOL Lightcited by 8
  2. 2016Encoding Monomorphic and Polymorphic Typescited by 2
  3. 2020Superposition for Lambda-Free Higher-Order Logiccited by 2
  4. 2015The computability path orderingcited by 1
  5. 2020Efficient Full Higher-Order Unificationcited by 1

Built on by

Cited by year

Citing papers per year: 2024: 1.

1 paper.

  1. 2024Superposition with Delayed Unificationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Optimistic Higher-Order Superposition
  2. 2023SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
  3. 2025L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL ↗
  4. 2022Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
  5. 2024The Existential Theory of the Reals with Summation Operators
  6. 2026A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
  7. 2025Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version) ↗
  8. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning