TY - GEN
T1 - Superposition with First-Class Booleans and Inprocessing Clausification
AU - Nummelin, V.
AU - Bentkamp, A.
AU - Tourret, S.
AU - Vukmirović, P.
PY - 2021
Y1 - 2021
N2 - © 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.
AB - © 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.
U2 - 10.1007/978-3-030-79876-5_22
DO - 10.1007/978-3-030-79876-5_22
M3 - Conference contribution
SN - 9783030798758
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 378
EP - 395
BT - Automated Deduction – CADE 2021
A2 - Platzer, A.
A2 - Sutcliffe, G.
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 -