Superposition with lambdas

Alexander Bentkamp*, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, 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 Deduction – CADE 2019
Subtitle of host publication27th International Conference on Automated Deduction, Proceedings
EditorsPascal Fontaine
PublisherSpringer
Pages55-73
Number of pages19
ISBN (Electronic)9783030294366
ISBN (Print)9783030294359
DOIs
Publication statusPublished - 2019
Event27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil
Duration: 27 Aug 201930 Aug 2019

Publication series

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

Conference

Conference27th International Conference on Automated Deduction, CADE 2019
CountryBrazil
CityNatal
Period27/08/1930/08/19

Fingerprint Dive into the research topics of 'Superposition with lambdas'. Together they form a unique fingerprint.

Cite this