Superposition with lambdas

Alexander Bentkamp; Jasmin Blanchette; Sophie Tourret; Petar Vukmirović; Uwe Waldmann

doi:10.1007/978-3-030-29436-6_4

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 proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Automated Deduction – CADE 2019
Subtitle of host publication	27th International Conference on Automated Deduction, Proceedings
Editors	Pascal Fontaine
Publisher	Springer
Pages	55-73
Number of pages	19
ISBN (Electronic)	9783030294366
ISBN (Print)	9783030294359
DOIs	https://doi.org/10.1007/978-3-030-29436-6_4
Publication status	Published - 2019
Event	27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil Duration: 27 Aug 2019 → 30 Aug 2019

Publication series

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

Conference

Conference	27th International Conference on Automated Deduction, CADE 2019
Country	Brazil
City	Natal
Period	27/08/19 → 30/08/19

Access to Document

10.1007/978-3-030-29436-6_4

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

Cite this

Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., & Waldmann, U. (2019). Superposition with lambdas. In P. Fontaine (Ed.), Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings (pp. 55-73). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI). Springer. https://doi.org/10.1007/978-3-030-29436-6_4

Bentkamp, Alexander ; Blanchette, Jasmin ; Tourret, Sophie ; Vukmirović, Petar ; Waldmann, Uwe. / Superposition with lambdas. Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings. editor / Pascal Fontaine. Springer, 2019. pp. 55-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6697892623f74794b6ce2066a5ef9226,

title = "Superposition with lambdas",

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

author = "Alexander Bentkamp and Jasmin Blanchette and Sophie Tourret and Petar Vukmirovi{\'c} and Uwe Waldmann",

year = "2019",

doi = "10.1007/978-3-030-29436-6_4",

language = "English",

isbn = "9783030294359",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "55--73",

editor = "Pascal Fontaine",

booktitle = "Automated Deduction – CADE 2019",

note = "27th International Conference on Automated Deduction, CADE 2019 ; Conference date: 27-08-2019 Through 30-08-2019",

}

Bentkamp, A , Blanchette, J, Tourret, S, Vukmirović, P & Waldmann, U 2019, Superposition with lambdas. in P Fontaine (ed.), Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11716 LNAI, Springer, pp. 55-73, 27th International Conference on Automated Deduction, CADE 2019, Natal, Brazil, 27/08/19. https://doi.org/10.1007/978-3-030-29436-6_4

Superposition with lambdas. / Bentkamp, Alexander ; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe.

Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings. ed. / Pascal Fontaine. Springer, 2019. p. 55-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Superposition with lambdas

AU - Bentkamp, Alexander

AU - Blanchette, Jasmin

AU - Tourret, Sophie

AU - Vukmirović, Petar

AU - Waldmann, Uwe

PY - 2019

Y1 - 2019

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

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

UR - http://www.scopus.com/inward/record.url?scp=85076984668&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076984668&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-29436-6_4

DO - 10.1007/978-3-030-29436-6_4

M3 - Conference contribution

AN - SCOPUS:85076984668

SN - 9783030294359

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 55

EP - 73

BT - Automated Deduction – CADE 2019

A2 - Fontaine, Pascal

PB - Springer

T2 - 27th International Conference on Automated Deduction, CADE 2019

Y2 - 27 August 2019 through 30 August 2019

ER -

Bentkamp A , Blanchette J, Tourret S, Vukmirović P, Waldmann U. Superposition with lambdas. In Fontaine P, editor, Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings. Springer. 2019. p. 55-73. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-29436-6_4