TY - GEN
T1 - A Unifying Splitting Framework
AU - Ebner, G.
AU - Blanchette, J.
AU - Tourret, S.
PY - 2021
Y1 - 2021
N2 - © 2021, The Author(s).AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.
AB - © 2021, The Author(s).AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers.
U2 - 10.1007/978-3-030-79876-5_20
DO - 10.1007/978-3-030-79876-5_20
M3 - Conference contribution
SN - 9783030798758
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 344
EP - 360
BT - Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings
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 -