A Unifying Splitting Framework

G. Ebner, J. Blanchette, S. Tourret

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

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.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE 28
Subtitle of host publication28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings
EditorsAndré Platzer, Geoff Sutcliffe
PublisherSpringer Science and Business Media Deutschland GmbH
Pages344-360
Number of pages17
ISBN (Electronic)9783030798765
ISBN (Print)9783030798758
DOIs
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)
Volume12699 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th International Conference on Automated Deduction, CADE 28 2021
CityVirtual, Online
Period12/07/2115/07/21

Fingerprint

Dive into the research topics of 'A Unifying Splitting Framework'. Together they form a unique fingerprint.

Cite this