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

© A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.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

Access to Document

10.23638/LMCS-17(2:1)2021

https://lmcs.episciences.org/7349

Handle.net

Persistent link

Cite this

@article{43315057ed8e46f88b57693618a9fe17,

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

abstract = "{\textcopyright} A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.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",

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 - © A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.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 - © A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann.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

Access to Document

Handle.net

Fingerprint

Cite this