- 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
http://profs.sci.univr.it/~bonacina/
- Id prodotto:
-
47518
- Handle IRIS:
-
11562/323520
- depositato il:
-
15 marzo 2012
- ultima modifica:
-
23 febbraio 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 
