Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp; Jasmin Christian Blanchette; Simon Cruanes; Uwe Waldmann

doi:10.23638/LMCS-17(2:1)2021

Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp
, Jasmin Christian Blanchette
, Simon Cruanes
, Uwe Waldmann

Research output: Contribution to Journal › Article › Academic › peer-review

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.

Original language	English
Article number	1
Pages (from-to)	1:1–1:38
Number of pages	38
Journal	Logical Methods in Computer Science
Volume	17
Issue number	2
DOIs	https://doi.org/10.23638/LMCS-17(2:1)2021
Publication status	Published - 12 Apr 2021

Bibliographical note

Funding

Acknowledgment. We are grateful to the maintainers of StarExec for letting us use their service. We want to thank Petar Vukmirović for his work on Zipperposition and for his advice. We thank Christoph Benzmüller, Sander Dahmen, Johannes Hölzl, Anders Schlichtkrull, Stephan Schulz, Alexander Steen, Geoff Sutcliffe, Andrei Voronkov, Daniel Wand, Christoph Weidenbach, and the participants in the 2017 Dagstuhl Seminar on Deduction beyond First-Order Logic for stimulating discussions. We also want to thank Christoph Benzmüller, Ahmed Bhayat, Wan Fokkink, Alexander Steen, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting several textual improvements. Bentkamp and Blanchette’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka).

Funders	Funder number
European Research Council
European Union?s Horizon 2020 research and innovation program	713999

Access to Document

10.23638/LMCS-17(2:1)2021

https://lmcs.episciences.org/7349

Persistent URL (handle)

Persistent link

Cite this

@article{43315057ed8e46f88b57693618a9fe17,

title = "Superposition for Lambda-Free Higher-Order Logic",

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.",

author = "Alexander Bentkamp and Blanchette, \{Jasmin Christian\} and Simon Cruanes and Uwe Waldmann",

note = "{\textcopyright} A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.",

year = "2021",

month = apr,

day = "12",

doi = "10.23638/LMCS-17(2:1)2021",

language = "English",

volume = "17",

pages = "1:1–1:38",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "2",

}

TY - JOUR

T1 - Superposition for Lambda-Free Higher-Order Logic

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin Christian

AU - Cruanes, Simon

AU - Waldmann, Uwe

PY - 2021/4/12

Y1 - 2021/4/12

N2 - 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.

AB - 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.

U2 - 10.23638/LMCS-17(2:1)2021

DO - 10.23638/LMCS-17(2:1)2021

M3 - Article

SN - 1860-5974

VL - 17

SP - 1:1–1:38

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

M1 - 1

ER -

Superposition for Lambda-Free Higher-Order Logic

Abstract

Bibliographical note

Funding

Access to Document

Persistent URL (handle)

Fingerprint

Cite this