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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
F. Baader and K. Schulz. Combination of constraint solving techniques: An algebraic point of view. In Proceedings 6th Conference on Rewriting Techniques and Applications, Kaiserslautern (Germany), volume 914 of Lecture Notes in Computer Science, pages 352–366. Springer-Verlag, 1995
F. Baader and K. Schulz. On the combination of symbolic constraints, solution domains, and constraint solvers. In Proceedings of the first International Conference on Principles and Practice of Constraint Programming - CP’95, Cassis (France), volume 976 of Lecture Notes in Computer Science, pages 380–397. Springer-Verlag, 1995
F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, Saratoga Springs (USA), volume 607 of Lecture Notes in Artificial Intelligence, pages 50–65. Springer-Verlag, June 15–18, 1992
F. Baader and K. Schulz. Combination techniques and decision problems for disunification. Theoretical Computer Science, 142:229–255, 1995
G. Birkhoff. On the structure of abstract algebras. Proceedings Cambridge Phil. Soc., 31:433–454,1935
A. Boudet, J.-P. Jouannaud, and M. Schmidt-Schauß. Unification in boolean rings and abelian groups. In C. Kirchner, editor, Unification, pages 267–296. Academic Press, London, 1990
E. Domenjoud, F. Klay, and Ch. Ringeissen. Combination techniques for non-disjoint equational theories. In Alan Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 267–281. Springer-Verlag, June/July 1994
A. Herold. Combination of Unification Algorithms in Equational Theories. PhD thesis, Universität Kaiserslautern (Germany), 1987
J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. The MIT press, Cambridge (MA, USA), 1991
H. Kirchner and Ch. Ringeissen. Combining symbolic constraint solvers on algebraic domains. Journal of Symbolic Computation, 18(2):113–155, 1994
G. Nelson. Techniques for program verification. Technical Report CS-81–10, Xerox Palo Research Center California USA, 1981
G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, l(2):245–257, October 1979
D. C. Oppen. Complexity, convexity and combinations of theories. Theoretical Computer Science, 12:291–302, 1980
Ch. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, St. Petersburg (Russia), volume 624 of Lecture Notes in Artificial Intelligence, pages 261–272. Springer-Verlag, 1992
Ch. Ringeissen. Combinaison de Résolutions de Contraintes. Thèse de Doctorat d’Université, Université de Nancy 1, December 1993
M. Schmidt-Schauß. Combination of unification algorithms. Journal of Symbolic Computation, 8(1 & 2):51–100, 1989. Special issue on unification. Part two
R. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2):351–360,1979
R. Shostak. Deciding combination of theories. Journal of the ACM, 31(1):1–12, 1984
E. Tidén. First-order unification in combinations of equational theories. PhD thesis, The Royal Institute of Technology, Stockholm, 1986
C. Tinelli. Extending the CLP scheme to unions of constraint theories. Master’s thesis, Department of Computer Science, University of Illinois, Urbana-Champaign, Illinois, October 1995
K. Yelick. Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation, 3(1 & 2):153–182, April 1987
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Science+Business Media New York
About this chapter
Cite this chapter
Ringeissen, C. (1996). Cooperation of Decision Procedures for the Satisfiability Problem. In: Baader, F., Schulz, K.U. (eds) Frontiers of Combining Systems. Applied Logic Series, vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-0349-4_6
Download citation
DOI: https://doi.org/10.1007/978-94-009-0349-4_6
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-6643-3
Online ISBN: 978-94-009-0349-4
eBook Packages: Springer Book Archive