Making Higher-Order Superposition Work

P. Vukmirović; A. Bentkamp; J. Blanchette; S. Cruanes; V. Nummelin; S. Tourret

doi:10.1007/978-3-030-79876-5_24

Making Higher-Order Superposition Work

P. Vukmirović
, A. Bentkamp
, J. Blanchette
, S. Cruanes
, V. Nummelin
, S. Tourret

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

Abstract

Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

Original language	English
Title of host publication	Automated Deduction – CADE 2021
Subtitle of host publication	28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings
Editors	André Platzer, Geoff Sutcliffe
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	415-432
Number of pages	18
ISBN (Electronic)	9783030798765
ISBN (Print)	9783030798758
DOIs	https://doi.org/10.1007/978-3-030-79876-5_24
Publication status	Published - 2021
Event	28th International Conference on Automated Deduction, CADE 28 2021 - Virtual, Online Duration: 12 Jul 2021 → 15 Jul 2021

Publication series

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

Name	CADE: International Conference on Automated Deduction
Publisher	Springer
Volume	2021

Conference

Conference	28th International Conference on Automated Deduction, CADE 28 2021
City	Virtual, Online
Period	12/07/21 → 15/07/21

Funding

We are grateful to the maintainers of StarExec for letting us use their service. Ahmed Bhayat and Giles Reger guided us through details of Vampire 4.5. Ahmed Bhayat, Michael F?rber, Mathias Fleury, Predrag Jani?i?, Mark Summerfield, and the anonymous reviewers suggested content, textual, and typesetting improvements. We thank them all. Vukmirovi?, 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). Blanchette and Nummelin?s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward) and the Incidental Financial Support scheme. Vukmirovi\u0107, Bentkamp, and Blanchette\u2019s research has received funding from the European Research Council (ERC) under the European Union\u2019s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Blanchette and Nummelin\u2019s research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward) and the Incidental Financial Support scheme.

Funders	Funder number
Incidental Financial Support scheme
Mathias Fleury
European Research Council
???publication-publication-funding-organisation-not-added???	016.Vidi.189.037, 016
Horizon 2020 Framework Programme	713999

Access to Document

10.1007/978-3-030-79876-5_24

Persistent URL (handle)

Persistent link

Cite this

Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., & Tourret, S. (2021). Making Higher-Order Superposition Work. In A. Platzer, & G. Sutcliffe (Eds.), Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings (pp. 415-432). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12699 LNAI), (CADE: International Conference on Automated Deduction; Vol. 2021). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-79876-5_24

Vukmirović, P. ; Bentkamp, A. ; Blanchette, J. et al. / Making Higher-Order Superposition Work. Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. editor / André Platzer ; Geoff Sutcliffe. Springer Science and Business Media Deutschland GmbH, 2021. pp. 415-432 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). (CADE: International Conference on Automated Deduction).

@inproceedings{5fa48785d37c4e25a9947a29143805d7,

title = "Making Higher-Order Superposition Work",

abstract = "Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.",

author = "P. Vukmirovi{\'c} and A. Bentkamp and J. Blanchette and S. Cruanes and V. Nummelin and S. Tourret",

year = "2021",

doi = "10.1007/978-3-030-79876-5\_24",

language = "English",

isbn = "9783030798758",

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

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "415--432",

editor = "Andr{\'e} Platzer and Geoff Sutcliffe",

booktitle = "Automated Deduction – CADE 2021",

note = "28th International Conference on Automated Deduction, CADE 28 2021 ; Conference date: 12-07-2021 Through 15-07-2021",

}

Vukmirović, P, Bentkamp, A, Blanchette, J, Cruanes, S, Nummelin, V & Tourret, S 2021, Making Higher-Order Superposition Work. in A Platzer & G Sutcliffe (eds), Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12699 LNAI, CADE: International Conference on Automated Deduction, vol. 2021, Springer Science and Business Media Deutschland GmbH, pp. 415-432, 28th International Conference on Automated Deduction, CADE 28 2021, Virtual, Online, 12/07/21. https://doi.org/10.1007/978-3-030-79876-5_24

Making Higher-Order Superposition Work. / Vukmirović, P.; Bentkamp, A.; Blanchette, J. et al.
Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. ed. / André Platzer; Geoff Sutcliffe. Springer Science and Business Media Deutschland GmbH, 2021. p. 415-432 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12699 LNAI), (CADE: International Conference on Automated Deduction; Vol. 2021).

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

TY - GEN

T1 - Making Higher-Order Superposition Work

AU - Vukmirović, P.

AU - Bentkamp, A.

AU - Blanchette, J.

AU - Cruanes, S.

AU - Nummelin, V.

AU - Tourret, S.

PY - 2021

Y1 - 2021

N2 - Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

AB - Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

U2 - 10.1007/978-3-030-79876-5_24

DO - 10.1007/978-3-030-79876-5_24

M3 - Conference contribution

SN - 9783030798758

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

SP - 415

EP - 432

BT - Automated Deduction – CADE 2021

A2 - Platzer, André

A2 - Sutcliffe, Geoff

PB - Springer Science and Business Media Deutschland GmbH

T2 - 28th International Conference on Automated Deduction, CADE 28 2021

Y2 - 12 July 2021 through 15 July 2021

ER -

Vukmirović P, Bentkamp A, Blanchette J, Cruanes S, Nummelin V, Tourret S. Making Higher-Order Superposition Work. In Platzer A, Sutcliffe G, editors, Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Springer Science and Business Media Deutschland GmbH. 2021. p. 415-432. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). (CADE: International Conference on Automated Deduction). Epub 2021 Jul 5. doi: 10.1007/978-3-030-79876-5_24

Making Higher-Order Superposition Work

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Fingerprint

Cite this