Superposition with Lambdas
This work addresses automated theorem proving for higher-order logic, which is incremental as it adapts superposition to a specific logical fragment.
The authors tackled the problem of automated reasoning in extensional polymorphic higher-order logic by designing a superposition calculus that handles anonymous functions, and they implemented it in the Zipperposition prover, showing it performs well on TPTP and Isabelle benchmarks.
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.