Publications

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:

January 31, 2023

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