# Superposition with Lambdas

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

## Key facts

- Cited by 1 papers 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 (most cited first, 5 of 5)

- [HOL(y)Hammer: Online ATP Service for HOL Light](https://mlsanity.com/paper/1309.4962/) (2013)
- [Encoding Monomorphic and Polymorphic Types](https://mlsanity.com/paper/1609.08916/) (2016)
- [Superposition for Lambda-Free Higher-Order Logic](https://mlsanity.com/paper/2005.02094/) (2020)
- [The computability path ordering](https://mlsanity.com/paper/1506.03943/) (2015)
- [Efficient Full Higher-Order Unification](https://mlsanity.com/paper/2011.09507/) (2020)

## Built on by (most cited first, 1 of 1)

- [Superposition with Delayed Unification](https://mlsanity.com/paper/2403.04775/) (2024)

## 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.