Superposition for Lambda-Free Higher-Order Logic - Archive ouverte HAL Access content directly
Journal Articles Logical Methods in Computer Science Year : 2021

Superposition for Lambda-Free Higher-Order Logic

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

Abstract

We introduce refutationally complete superposition calculi for intentional and extensional clausal λ-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the λ-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
Fichier principal
Vignette du fichier
lfhosup_article.pdf (759.1 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

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

Identifiers

Cite

Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann. Superposition for Lambda-Free Higher-Order Logic. Logical Methods in Computer Science, 2021, 17 (2), ⟨10.23638/LMCS-17(2:1)2021⟩. ⟨hal-03485227⟩
35 View
23 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More