Cooperation of Decision Procedures for the Satisfiability Problem

Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Constraint programming is strongly based on the use of solvers which are able to check satisfiability of constraints. We show in this paper a rule-based algorithm for solving in a modular way the satisfiability problem w.r.t. a class of theories $Th$. The case where $Th$ is the union of two disjoint theories $Th_1$ and $Th_2$ is known for a long time but we study here different cases where function symbols are shared by $Th_1$ and $Th_2$. The chosen approach leads to a highly non-deterministic decomposition algorithm but drastically simplifies the understanding of the combination problem. The obtained decomposition algorithm is illustrated by the combination of non-disjoint equational theories.
Type de document :
Rapport
[Research Report] RR-2753, INRIA. 1995, pp.19
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00073939
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:07:50
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:02:09

Fichiers

Identifiants

  • HAL Id : inria-00073939, version 1

Collections

Citation

Christophe Ringeissen. Cooperation of Decision Procedures for the Satisfiability Problem. [Research Report] RR-2753, INRIA. 1995, pp.19. 〈inria-00073939〉

Partager

Métriques

Consultations de la notice

153

Téléchargements de fichiers

134