Making Higher-Order Superposition Work

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

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


© 2021, The Author(s).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 languageEnglish
Title of host publicationAutomated Deduction – CADE 2021
Subtitle of host publication28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings
EditorsAndré Platzer, Geoff Sutcliffe
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages18
ISBN (Electronic)9783030798765
ISBN (Print)9783030798758
Publication statusPublished - 2021
Event28th International Conference on Automated Deduction, CADE 28 2021 - Virtual, Online
Duration: 12 Jul 202115 Jul 2021

Publication series

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


Conference28th International Conference on Automated Deduction, CADE 28 2021
CityVirtual, Online


Dive into the research topics of 'Making Higher-Order Superposition Work'. Together they form a unique fingerprint.

Cite this