- Authors:
-
Bonacina, Maria Paola; Mnacho, Echenim
- Title:
-
Theory decision by decomposition
- Year:
-
2010
- Type of item:
-
Articolo in Rivista
- Tipologia ANVUR:
- Articolo su rivista
- Language:
-
Inglese
- Format:
-
A Stampa
- Referee:
-
Sì
- Name of journal:
- Journal of Symbolic Computation
- ISSN of journal:
- 0747-7171
- N° Volume:
-
45
- Number or Folder:
-
2
- :
- Elsevier
- Page numbers:
-
229-260
- Keyword:
-
Satisfiability modulo theories; decision procedures; combination of theories; rewrite-based theorem proving; superposition; paramodulation
- Short description of contents:
- 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.
- Web page:
-
http://dx.doi.org/10.1016/j.jsc.2008.10.008; http://profs.sci.univr.it/~bonacina/
- Product ID:
-
47518
- Handle IRIS:
-
11562/323520
- Deposited On:
-
March 15, 2012
- Last Modified:
-
August 16, 2021
- Bibliographic citation:
-
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 
