Superposition with Lambdas - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2021

Superposition with Lambdas

(1) , (2, 3) , (4, 3, 5) , (1) , (4)
1
2
3
4
5

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 $\beta \eta$-equivalence classes of $\lambda$-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.
Fichier principal
Vignette du fichier
lamsup_article.pdf (421.08 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03485185 , version 1 (17-12-2021)

Identifiers

Cite

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann. Superposition with Lambdas. Journal of Automated Reasoning, 2021, 65 (7), pp.893-940. ⟨10.1007/s10817-021-09595-y⟩. ⟨hal-03485185⟩
17 View
28 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More