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

69 Downloads (Pure)

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, Natal, Brazil, August 27–30, 2019, 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/Territory	Brazil
City	Natal
Period	27/08/19 → 30/08/19

Funding

Simon Cruanes patiently explained Zipperposition?s internals and allowed us to continue the development of his prover. Christoph Benzm?ller and Alexander Steen shared insights and examples with us, guiding us through the literature and clarifying how the Leos work. Maria Paola Bonacina and Nicolas Peltier gave us some ideas on how to treat the extensionality axiom as a theory axiom, ideas we have yet to explore. Mathias Fleury helped us set up regression tests for Zipperposition. Ahmed Bhayat, Tomer Libal, and Enrico Tassi shared their insights on higher-order unification. Andrei Popescu and Dmitriy Traytel explained the terminology surrounding the ?-calculus. Haniel Barbosa, Daniel El Ouraoui, Pascal Fontaine, and Hans-J?rg Schurr were involved in many stimulating discussions. Christoph Weidenbach made this collaboration possible. Ahmed Bhayat, Mark Summerfield, and the anonymous reviewers suggested several textual improvements. We thank them all. Bentkamp, Blanchette, and Vukmirovi??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). Bentkamp and Blanchette also benefited from the Netherlands Organization for Scientific Research (NWO) Incidental Financial Support scheme. Blanchette has received funding from the NWO under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

Funders	Funder number
Horizon 2020 Framework Programme	713999
European Research Council
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	016

Access to Document

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

Superposition with LambdasFinal published version, 504 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

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, Natal, Brazil, August 27–30, 2019, 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 et al. / Superposition with lambdas. Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, 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, Natal, Brazil, August 27–30, 2019, 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 et al.
Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, 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, Natal, Brazil, August 27–30, 2019, Proceedings. Springer. 2019. p. 55-73. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2019 Aug 20. doi: 10.1007/978-3-030-29436-6_4

Superposition with lambdas

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this