Pubblicazioni

Theory decision by decomposition  (2010)

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:
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:
15 novembre 2022
Citazione bibliografica:
Bonacina, Maria Paola; Mnacho, Echenim, Theory decision by decomposition «Journal of Symbolic Computation» , vol. 45 , n. 22010pp. 229-260

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

Progetti Collegati
Titolo Dipartimento Responsabili
Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti - Progetto ed integrazione di macchine di prova per l'analisi di programmi (PRIN 2007) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture