Unions of non-disjoint theories and combinations of satisfiability procedures. (English) Zbl 1018.68033
Summary: 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.
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Keywords:
combination of satisfiability procedures; decision problems; constraint-based reasoning; automated deductionReferences:
| [1] | A. Armando, S. Ranise, Constraint contextual rewriting, in: R. Caferra, G. Salzer (Eds.), Proc. 2nd Internat. Workshop on First Order Theorem Proving, FTP��98, Vienna, Austria, 1998, pp. 65-75.; A. Armando, S. Ranise, Constraint contextual rewriting, in: R. Caferra, G. Salzer (Eds.), Proc. 2nd Internat. Workshop on First Order Theorem Proving, FTP’98, Vienna, Austria, 1998, pp. 65-75. · Zbl 1039.68059 |
| [2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press UK |
| [3] | F. Baader, K.U. Schulz, Combination of constraint solving techniques: an algebraic point of view, Proc. 6th Internat. Conf. on Rewriting Techniques and Applications, RTA’95, Lecture Notes in Computer Science, Vol. 914, Springer, Berlin, 1995a, pp. 50-65.; F. Baader, K.U. Schulz, Combination of constraint solving techniques: an algebraic point of view, Proc. 6th Internat. Conf. on Rewriting Techniques and Applications, RTA’95, Lecture Notes in Computer Science, Vol. 914, Springer, Berlin, 1995a, pp. 50-65. |
| [4] | Baader, F.; Schulz, K. U., Combination techniques and decision problems for disunification, Theoret. Comput. Sci., 142, 229-255 (1995) · Zbl 0873.68188 |
| [5] | F. Baader, K.U. Schulz, On the combination of symbolic constraints, solution domains, and constraint solvers, in: Proc. First Internat. Conf. on Principles and Practice of Constraint Programming, Cassis, France, Lecture Notes in Artificial Intelligence, Vol. 976, Springer, Berlin, 1995c.; F. Baader, K.U. Schulz, On the combination of symbolic constraints, solution domains, and constraint solvers, in: Proc. First Internat. Conf. on Principles and Practice of Constraint Programming, Cassis, France, Lecture Notes in Artificial Intelligence, Vol. 976, Springer, Berlin, 1995c. |
| [6] | Baader, F.; Schulz, K. U., Unification in the union of disjoint equational theoriescombining decision procedures, J. Symbolic Comput., 21, 2, 211-243 (1996) · Zbl 0851.68055 |
| [7] | Baader, F.; Schulz, K. U., Combination of constraint solvers for free and quasi-free structures, Theoret. Comput. Sci., 192, 107-161 (1998) · Zbl 0895.68019 |
| [8] | Baader, F.; Tinelli, C., A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, (McCune, W., Proc. 14th Internat. Conf. on Automated Deduction, Townsville, Australia. Proc. 14th Internat. Conf. on Automated Deduction, Townsville, Australia, Lecture Notes in Artificial Intelligence, Vol. 1249 (1997), Springer: Springer Berlin), 19-33 · Zbl 1430.03036 |
| [9] | F. Baader, C. Tinelli, Deciding the word problem in the union of equational theories, Tech. Report UIUCDCS-R-98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, October 1998.; F. Baader, C. Tinelli, Deciding the word problem in the union of equational theories, Tech. Report UIUCDCS-R-98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, October 1998. · Zbl 1049.03032 |
| [10] | Baader, F.; Tinelli, C., Deciding the word problem in the union of equational theories sharing constructors, (Narendran, P.; Rusinowitch, M., Proc. 10th Internat. Conf. on Rewriting Techniques and Applications, Trento, Italy. Proc. 10th Internat. Conf. on Rewriting Techniques and Applications, Trento, Italy, Lecture Notes in Computer Science, Vol. 1631 (1999), Springer: Springer Berlin), 175-189 · Zbl 0976.03051 |
| [11] | F. Baader, C. Tinelli, Deciding the word problem in the union of equational theories, Inform. and Comput. (2001), to appear.; F. Baader, C. Tinelli, Deciding the word problem in the union of equational theories, Inform. and Comput. (2001), to appear. · Zbl 1049.03032 |
| [12] | P. Baumgartner, U. Furbach, U. Petermann, A unified approach to theory reasoning, Research Report 15-92, Universität Koblenz-Landau, Koblenz, Germany, fachberichte Informatik, 1992.; P. Baumgartner, U. Furbach, U. Petermann, A unified approach to theory reasoning, Research Report 15-92, Universität Koblenz-Landau, Koblenz, Germany, fachberichte Informatik, 1992. |
| [13] | Boudet, A., Combining unification algorithms, J. Symbolic Comput., 16, 6, 597-626 (1993) · Zbl 0822.68054 |
| [14] | Bürckert, H.-J., A resolution principle for constraint logics, Artif. Intell., 66, 235-271 (1994) · Zbl 0807.68082 |
| [15] | Dershowitz, N.; Jouannaud, J.-P., Rewriting systems, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), Elsevier Publishers: Elsevier Publishers Amsterdam), 243-320 · Zbl 0900.68283 |
| [16] | Domenjoud, E.; Klay, F.; Ringeissen, C., Combination techniques for non-disjoint equational theories, (Bundy, A., Proc. 12th Internat. Conf. on Automated Deduction, Nancy, France. Proc. 12th Internat. Conf. on Automated Deduction, Nancy, France, Lecture Notes in Artificial Intelligence, Vol. 814 (1994), Springer: Springer Berlin), 267-281 · Zbl 1433.68544 |
| [17] | H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, Vol. 6, Springer, Berlin, 1985, New York, NY.; H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, Vol. 6, Springer, Berlin, 1985, New York, NY. · Zbl 0557.68013 |
| [18] | H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, EATCS Monographs on Theoretical Computer Science, Vol. 21, Springer, Berlin, 1990, New York, NY.; H. Ehrig, B. Mahr, Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, EATCS Monographs on Theoretical Computer Science, Vol. 21, Springer, Berlin, 1990, New York, NY. · Zbl 0759.68013 |
| [19] | C. Fiorentini, S. Ghilardi, Combining word problems through rewriting in categories with products, Theoret. Comput. Sci. (2001), to appear.; C. Fiorentini, S. Ghilardi, Combining word problems through rewriting in categories with products, Theoret. Comput. Sci. (2001), to appear. · Zbl 1028.68070 |
| [20] | Goguen, J. A.; Meseguer, J., Order sorted algebra I. Equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoret. Comput. Sci., 105, 2, 217-273 (1992) · Zbl 0778.68056 |
| [21] | Gramlich, B., On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Theoret. Comput. Sci., 165, 1, 97-131 (1996) · Zbl 0872.68081 |
| [22] | Herold, J., Combination of unification algorithms, (Siekmann, J., Proc. 8th Internat. Conf. on Automated Deduction, Oxford (UK). Proc. 8th Internat. Conf. on Automated Deduction, Oxford (UK), Lecture Notes in Artificial Intelligence, Vol. 230 (1986), Springer: Springer Berlin), 450-469 · Zbl 0643.68137 |
| [23] | Hodges, W., Model Theory. Model Theory, Enclyclopedia of Mathematics and its Applications, Vol. 42 (1993), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0789.03031 |
| [24] | M. Höhfeld, G. Smolka, Definite relations over constraint languages, LILOG Report 53, IWBS, IBM Deutschland, Postfach 80 08 80, 7000 Stuttgart 80, Germany, 1988.; M. Höhfeld, G. Smolka, Definite relations over constraint languages, LILOG Report 53, IWBS, IBM Deutschland, Postfach 80 08 80, 7000 Stuttgart 80, Germany, 1988. |
| [25] | Holland, K. L., An introduction to fusions of strongly minimal sets: the geometry of fusions, Arch. Math. Logic, 34, 395-413 (1995) · Zbl 0849.03020 |
| [26] | Jaffar, J.; Maher, M., Constraint logic programming: a survey, J. Logic Programming, 19/20, 503-581 (1994) |
| [27] | J.-P. Jouannaud, H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput. 15(4) (1986) 1155-1194, preliminary version in Proc. 11th ACM Symp. on Principles of Programming Languages, Salt Lake City, USA, 1984.; J.-P. Jouannaud, H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput. 15(4) (1986) 1155-1194, preliminary version in Proc. 11th ACM Symp. on Principles of Programming Languages, Salt Lake City, USA, 1984. · Zbl 0665.03005 |
| [28] | Kepser, S.; Schulz, K. U., Combination of constraint systems II: Rational amalgamation, (Freuder, E. C., Proc. 2nd Internat. Conf. on Principles and Practice of Constraint Programming, Cambridge, MA, USA. Proc. 2nd Internat. Conf. on Principles and Practice of Constraint Programming, Cambridge, MA, USA, Lecture Notes in Computer Science, Vol. 1118 (1996), Springer: Springer Berlin), 282-296 · Zbl 0992.68192 |
| [29] | Kirchner, C.; Kirchner, H.; Rusinowitch, M., Deduction with symbolic constraints (special issue on Automatic Deduction), Rev. Française Intell. Artif., 4, 3, 9-52 (1990) |
| [30] | Kirchner, H.; Ringeissen, C., Combining symbolic constraint solvers on algebraic domains, J. Symbolic Comput., 18, 2, 113-155 (1994) · Zbl 0819.68111 |
| [31] | Kirchner, H.; Ringeissen, C., Constraint solving by narrowing in combined algebraic domains, (Van Hentenryck, P., Proc. 11th Internat. Conf. on Logic Programming (1994), The MIT Press: The MIT Press Cambridge, MA), 617-631 |
| [32] | G. Nelson, Combining satisfiability procedures by equality-sharing,in: W.W. Bledsoe, D.W. Loveland (Eds.), Automated Theorem Proving: After 25 Years,Contemporary Mathematics. American Mathematical Society, Vol. 29, Providence, RI, 1984, pp. 201-211.; G. Nelson, Combining satisfiability procedures by equality-sharing,in: W.W. Bledsoe, D.W. Loveland (Eds.), Automated Theorem Proving: After 25 Years,Contemporary Mathematics. American Mathematical Society, Vol. 29, Providence, RI, 1984, pp. 201-211. · Zbl 0564.03011 |
| [33] | Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Programming Languages Systems, 1, 2, 245-257 (1979) · Zbl 0452.68013 |
| [34] | Nipkow, T., Combining matching algorithmsthe regular case, J. Symbolic Comput., 12, 633-653 (1991) · Zbl 0767.68069 |
| [35] | Ohlebusch, E., Modular properties of composable term rewriting systems, J. Symbolic Comput., 20, 1, 1-41 (1995) · Zbl 0851.68058 |
| [36] | Oppen, D. C., Complexity, convexity and combinations of theories, Theoret. Comput. Sci., 12, 291-302 (1980) · Zbl 0437.03007 |
| [37] | Pillay, A.; Tsuboi, A., Amalgamations preserving \(ℵ0\)-categoricity, The J. Symbolic Logic, 62, 4, 1070-1074 (1997) · Zbl 0899.03025 |
| [38] | Ringeissen, C., Unification in a combination of equational theories with shared constants and its application to primal algebras, (Voronkov, A., Proc. 1st Internat. Conf. on Logic Programming and Automated Reasoning. Proc. 1st Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, Vol. 624 (1992), Springer: Springer Berlin), 261-272 · Zbl 0920.08001 |
| [39] | C. Ringeissen, Combinaison de résolutions de contraines, Thèse de Doctorat d’ Université, Université de Nancy 1, Nancy, France, 1993.; C. Ringeissen, Combinaison de résolutions de contraines, Thèse de Doctorat d’ Université, Université de Nancy 1, Nancy, France, 1993. |
| [40] | Ringeissen, C., Combining decision algorithms for matching in the union of disjoint equational theories, Inform. and Comput., 126, 2, 144-160 (1996) · Zbl 0853.68105 |
| [41] | Ringeissen, C., Cooperation of decision procedures for the satisfiability problem, (Baader, F.; Schulz, K., Frontiers of Combining Systems: Proc. 1st Internat. Workshop, Munich, Germany, Applied Logic (1996), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 121-140 · Zbl 0945.03011 |
| [42] | M. Schmidt-Schauß, Unification in a combination of arbitrary disjoint equational theories, J. Symbolic Comput. 8 (1-2) (1989) 51-100, special issue on unification. Part II.; M. Schmidt-Schauß, Unification in a combination of arbitrary disjoint equational theories, J. Symbolic Comput. 8 (1-2) (1989) 51-100, special issue on unification. Part II. · Zbl 0691.03003 |
| [43] | Schulz, K. U., Why combined decision problems are often intractable, (Kirchner, H.; Ringeissen, C., Proc. 3rd Internat. Workshop on Frontiers of Combining Systems, FroCoS’2000, Nancy, France. Proc. 3rd Internat. Workshop on Frontiers of Combining Systems, FroCoS’2000, Nancy, France, Lecture Notes in Artificial Intelligence, Vol. 1794 (2000), Springer: Springer Berlin), 217-244 · Zbl 0961.03011 |
| [44] | Shostak, R. E., A practical decision procedure for arithmetic with function symbols, J. ACM, 26, 2, 351-360 (1979) · Zbl 0496.03003 |
| [45] | Shostak, R. E., Deciding combinations of theories, J. ACM, 31, 1-12 (1984) · Zbl 0629.68089 |
| [46] | C. Tinelli, Combination of decidability procedures for automated deduction and constraint-based reasoning, Ph.D. Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana-Champaign, Illinois, 1999.; C. Tinelli, Combination of decidability procedures for automated deduction and constraint-based reasoning, Ph.D. Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana-Champaign, Illinois, 1999. |
| [47] | Tinelli, C.; Harandi, M. T., A new correctness proof of the Nelson-Oppen combination procedure, (Baader, F.; Schulz, K., Frontiers of Combining Systems: Proc. 1st Internat. Workshop, Munich, Germany, Applied Logic (1996), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 103-120 · Zbl 0893.03001 |
| [48] | C. Tinelli, C. Ringeissen, Non-disjoint unions of theories and combinations of satisfiability procedures: first results, Tech. Report UIUCDCS-R-98-2044, Department of Computer Science, University of Illinois at Urbana-Champaign, 1998 (also available as INRIA research report no. RR-3402).; C. Tinelli, C. Ringeissen, Non-disjoint unions of theories and combinations of satisfiability procedures: first results, Tech. Report UIUCDCS-R-98-2044, Department of Computer Science, University of Illinois at Urbana-Champaign, 1998 (also available as INRIA research report no. RR-3402). · Zbl 1018.68033 |
| [49] | C. Tinelli, C. Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Tech. Report 01-02, Department of Computer Science, University of Iowa, 2001 (extended version of this paper).; C. Tinelli, C. Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Tech. Report 01-02, Department of Computer Science, University of Iowa, 2001 (extended version of this paper). · Zbl 1018.68033 |
| [50] | Wechler, W., Universal Algebra for Computer Scientists. Universal Algebra for Computer Scientists, EATCS Monographs on Theoretical Computer Science, Vol. 25 (1992), Springer: Springer Berlin, Heidelberg, New York · Zbl 0748.68002 |
| [51] | Wolter, F., Fusions of modal logics revisited, (Kracht, M.; de Rijke, M.; Wansing, H.; Zakharyaschev, M., Advances in Modal Logic, CSLI (1998), Stanford: Stanford CA) · Zbl 0956.03512 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
