Journal article
Unions of non-disjoint theories and combinations of satisfiability procedures
Theoretical computer science, Vol.290(1), pp.291-353
2003
DOI: 10.1016/S0304-3975(01)00332-2
Abstract
In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory
T
1
and one that decides constraint satisfiability with respect to a constraint theory
T
2
, produces a procedure that (semi-)decides constraint satisfiability with respect to the union of
T
1
and
T
2
. We provide a number of model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of the component theories are non-disjoint. We also describe some general classes of theories to which our combination results apply, and relate our approach to some of the existing combination methods in the field.
Details
- Title: Subtitle
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Creators
- Cesare Tinelli - University of IowaChristophe Ringeissen - Institut national de recherche en sciences et technologies du numérique
- Resource Type
- Journal article
- Publication Details
- Theoretical computer science, Vol.290(1), pp.291-353
- DOI
- 10.1016/S0304-3975(01)00332-2
- ISSN
- 0304-3975
- eISSN
- 1879-2294
- Publisher
- Elsevier B.V
- Language
- English
- Date published
- 2003
- Academic Unit
- Computer Science
- Record Identifier
- 9984259500902771
Metrics
7 Record Views