Pubblicazioni

Autori:

Bonacina, Maria Paola; Mnacho, Echenim

Titolo:

Theory decision by decomposition

Anno:

2010

Tipologia prodotto:

Articolo in Rivista

Tipologia ANVUR:

Articolo su rivista

Lingua:

Inglese

Formato:

A Stampa

Referee:

Sì

Nome rivista:

Journal of Symbolic Computation

ISSN Rivista:

0747-7171

N° Volume:

45

Numero o Fascicolo:

2

Editore:

Elsevier

Intervallo pagine:

229-260

Parole chiave:

Satisfiability modulo theories; decision procedures; combination of theories; rewrite-based theorem proving; superposition; paramodulation

Breve descrizione dei contenuti:

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulae. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based first-order theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis-Putnam-Logemann-Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories.

Pagina Web:

http://dx.doi.org/10.1016/j.jsc.2008.10.008
https://mariapaola.github.io/

Id prodotto:

47518

Handle IRIS:

11562/323520

depositato il:

15 marzo 2012

ultima modifica:

15 settembre 2023

Citazione bibliografica:

Bonacina, Maria Paola; Mnacho, Echenim, Theory decision by decomposition «Journal of Symbolic Computation» , vol. 45 , n. 2 , 2010 , pp. 229-260

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo