Cargando…
Unifying Splitting
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., superpos...
| Autores principales: | , , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer Netherlands
2023
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10147822/ https://www.ncbi.nlm.nih.gov/pubmed/37131534 http://dx.doi.org/10.1007/s10817-023-09660-8 |