# Non-Disjoint Unions of Theories and Combinations of Satisfiability Procedures: First Results

Non-Disjoint Unions of Theories and Combinations of Satisfiability Procedures: First Results - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 PROTHEO - Constraints, automatic deduction and software properties proofs INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Abstract : In this paper we outline a theoretical framework for the combination of decision procedures for the satisfiability of constraints with respect to a constrainttheory. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory ${\cal T} 1$ and one that decides constraint satisfiability with respect to a constraint theory ${\cal T} 2$, is able to produce a procedure that semi-decides constraint satisfiability with respect to the union of ${\cal T} 1$ and ${\cal T} 2$. We also provide some 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 ${\cal T} 1$ and ${\cal T} 2$ are non-disjoint.

Keywords : combination of satisfiability procedures decision problems constraint-based reasoning automated deduction

Autor: Cesare Tinelli Christophe Ringeissen -

Fuente: https://hal.archives-ouvertes.fr/

DESCARGAR PDF