Superposition for Lambda-Free Higher-Order Logic

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

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

13 Downloads (Pure)

Abstract

We introduce refutationally complete superposition calculi for intentional and extensional λ-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 TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.
Original languageEnglish
Title of host publicationAutomated Reasoning
Subtitle of host publication9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
EditorsDidier Galmiche, Stephan Schulz, Roberto Sebastiani
PublisherSpringer/Verlag
Pages28-46
Number of pages18
ISBN (Electronic)9783319942056
ISBN (Print)9783319942049
DOIs
Publication statusPublished - 2018
Event9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume10900 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/TerritoryUnited Kingdom
CityOxford
Period14/07/1817/07/18

Funding

Acknowledgment. We are grateful to the maintainers of StarExec for letting us use their service. We want to thank Christoph Benzmüller, Sander Dahmen, Johannes Hölzl, Anders Schlichtkrull, Stephan Schulz, Alexander Steen, Geoff Sutcliffe, Andrei Voronkov, Petar Vukmirović, 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 Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting several textual improvements to this paper and to the technical report. 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).

FundersFunder number
European Union’s Horizon 2020 research and innovation program
Horizon 2020 Framework Programme713999
European Research Council

    Fingerprint

    Dive into the research topics of 'Superposition for Lambda-Free Higher-Order Logic'. Together they form a unique fingerprint.

    Cite this