@inproceedings{cfdbb3afc87c4efca57987d8d47bf676,
title = "Boolean reasoning in a higher-order superposition prover",
abstract = "We present a pragmatic approach to extending a Boolean-free higher-order superposition calculus to support Boolean reasoning. Our approach extends inference rules that have been used only in a firstorder setting, uses some well-known rules previously implemented in higher-order provers, as well as new rules. We have implemented the approach in the Zipperposition theorem prover. The evaluation shows highly competitive performance of our approach and clear improvement over previous techniques.",
keywords = "Higher-order logic, Superposition, Theorem proving",
author = "Petar Vukmirovic and Visa Nummelin",
year = "2020",
month = nov,
day = "26",
language = "English",
series = "CEUR Workshop Proceedings",
publisher = "CEUR-WS",
pages = "148--166",
editor = "Pascal Fontaine and Konstantin Korovin and Kotsireas, {Ilias S.} and Philipp R{\"u}mmer and Sophie Tourret",
booktitle = "PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020",
note = "Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 ; Conference date: 05-07-2020",
}