Skip to Main content Skip to Navigation
Conference papers

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.
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 : Tuesday, March 3, 2020 - 4:07:50 PM
Document(s) archivé(s) le : Sunday, February 9, 2020 - 4:05:52 PM

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. CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.55-73, ⟨10.1007/978-3-030-29436-6_4⟩. ⟨hal-02296038⟩

Share

Metrics

Record views

93

Files downloads

380