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

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 βη-equivalence classes of
λ-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.
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)
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
CountryUnited Kingdom
CityOxford
Period14/07/1817/07/18

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

  • Cite this

    Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2018). Superposition for Lambda-Free Higher-Order Logic. In D. Galmiche, S. Schulz, & R. Sebastiani (Eds.), Automated Reasoning: 9th International Joint Conference, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 14–17, 2018 Proceedings (pp. 28-46). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI). Springer/Verlag. https://doi.org/10.1007/978-3-319-94205-6_3