Superposition with Lambdas

Abstract : 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 refuta-tional 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.
Document type :
Book sections
Complete list of metadatas

Cited literature [64 references]  Display  Hide  Download

https://hal.inria.fr/hal-02296038
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, September 24, 2019 - 5:17:54 PM
Last modification on : Friday, October 4, 2019 - 10:07:05 AM

File

conf.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann. Superposition with Lambdas. Automated Deduction – CADE 27. CADE 2019, pp.55-73, 2019, ⟨10.1007/978-3-030-29436-6_4⟩. ⟨hal-02296038⟩

Share

Metrics

Record views

64

Files downloads

264