Superposition with First-Class Booleans and Inprocessing Clausification

V. Nummelin, A. Bentkamp, S. Tourret, P. Vukmirović

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


© 2021, The Author(s).We present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE 2021
Subtitle of host publication28th International Conference on Automated Deduction, Proceedings
EditorsA. Platzer, G. Sutcliffe
PublisherSpringer Science and Business Media Deutschland GmbH
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)
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 'Superposition with First-Class Booleans and Inprocessing Clausification'. Together they form a unique fingerprint.

Cite this