A Unifying Splitting Framework

Gabriel Ebner (1) , Jasmin Blanchette (2, 3, 1) , Sophie Tourret (2, 4, 5)

1 VU - Vrije Universiteit Amsterdam [Amsterdam]
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 Computer Systems Section - Vrije Universiteit Amsterdam
4 MPII - Max-Planck-Institut für Informatik
5 MOSEL - Proof-oriented development of computer-based systems

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.

Domaines: Logique en informatique [cs.LO]

Gabriel Ebner, Jasmin Blanchette, Sophie Tourret. A Unifying Splitting Framework. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.344-360, ⟨10.1007/978-3-030-79876-5_20⟩. ⟨hal-03364063⟩