@inproceedings{a23f7c307b844bfd833e5e28e9263e43,
title = "A Unifying Splitting Framework",
abstract = "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.",
author = "G. Ebner and J. Blanchette and S. Tourret",
year = "2021",
doi = "10.1007/978-3-030-79876-5_20",
language = "English",
isbn = "9783030798758",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "344--360",
editor = "Andr{\'e} Platzer and Geoff Sutcliffe",
booktitle = "Automated Deduction – CADE 28",
note = "28th International Conference on Automated Deduction, CADE 28 2021 ; Conference date: 12-07-2021 Through 15-07-2021",
}