Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2023;67(2):16.
doi: 10.1007/s10817-023-09660-8. Epub 2023 Apr 28.

Unifying Splitting

Gabriel Ebner  1 , Jasmin Blanchette  1   2   3 , Sophie Tourret  2   3
Affiliations

Unifying Splitting

Gabriel Ebner et al. J Autom Reason. 2023.

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 that 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.

Keywords: AVATAR; Automated theorem proving; Completeness; Splitting.

PubMed Disclaimer

Figures

Fig. 1
Fig. 1
A split tree with a single infinite branch
Fig. 2
Fig. 2
A split tree with two infinite branches
See this image and copyright information in PMC

References

    1. Bachmair L, Ganzinger H. Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 1994;4(3):217–247. doi: 10.1093/logcom/4.3.217. - DOI
    1. Bachmair L, Ganzinger H. Resolution theorem proving. In: Robinson A, Voronkov A, editors. Handbook of Automated Reasoning. Amsterdam: Elsevier; 2001. pp. 19–99.
    1. Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C. CVC4. In: Gopalakrishnan G, Qadeer S, editors. CAV 2011. Berlin: Springer; 2011. pp. 171–177.
    1. Bjø[r]ner, N., Reger, G., Suda, M., Voronkov, A.: AVATAR modulo theories. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. EPiC Series in Computing, vol. 41, pp. 39–52. EasyChair, Manchester (2016)
    1. Bonacina MP, Plaisted DA. SGGS theorem proving: an exposition. In: Schulz S, de Moura L, Konev B, editors. PAAR-2014. Manchester: EasyChair; 2014. pp. 25–38.

LinkOut - more resources