Combination of convex theories: modularity, deduction completeness, and explanation. (English) Zbl 1192.68190
Summary: Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple “sat/unsat” answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.
MSC:
| 68P05 | Data structures |
Keywords:
decision procedure; combination; deduction completeness; conflict set; satisfiability modulo theoriesReferences:
| [1] | Armando, A.; Bonacina, M. P.; Ranise, S.; Schulz, S., New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, 10, 1 (2009) · Zbl 1367.68243 |
| [2] | Armando, A.; Ranise, S.; Rusinowitch, M., A rewriting approach to satisfiability procedures, Journal of Information and Computation, 183, 2, 140-164 (2003) · Zbl 1054.68077 |
| [3] | Bachmair, L.; Tiwari, A.; Vigneron, L., Abstract congruence closure, Journal of Automated Reasoning, 31, 2, 129-168 (2003) · Zbl 1040.03006 |
| [4] | Badros, G. J.; Borning, A.; Stuckey, P. J., The cassowary linear arithmetic constraint solving algorithm, ACM Transactions on Computer Human Interaction, 8, 4, 267-306 (2001) |
| [5] | Barrett, C. W.; Dill, D. L.; Stump, A., A generalization of Shostak’s method for combining decision procedures, (Armando, A., Proc. of the 4th International Workshop on Frontiers of Combining Systems. Proc. of the 4th International Workshop on Frontiers of Combining Systems, FroCoS’02, Santa Margherita Ligure, Italy. Proc. of the 4th International Workshop on Frontiers of Combining Systems. Proc. of the 4th International Workshop on Frontiers of Combining Systems, FroCoS’02, Santa Margherita Ligure, Italy, LNCS, vol. 2309 (2002), Springer), 132-147 · Zbl 1057.68109 |
| [6] | Bonacina, M. P.; Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures, (Proc. of the 3rd Int. Conference on Automated Reasoning. Proc. of the 3rd Int. Conference on Automated Reasoning, IJCAR’06, Seattle, WA, USA. Proc. of the 3rd Int. Conference on Automated Reasoning. Proc. of the 3rd Int. Conference on Automated Reasoning, IJCAR’06, Seattle, WA, USA, LNAI, vol. 4130 (2006), Springer), 513-527 · Zbl 1222.03011 |
| [7] | Boudet, A., Combining unification algorithms, Journal of Symbolic Computation, 16, 6, 597-626 (1993) · Zbl 0822.68054 |
| [8] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T.; van Rossum, P.; Ranise, S.; Sebastiani, R., Efficient theory combination via boolean search, Information and Computation, 204, 10, 1493-1525 (2006) · Zbl 1137.68578 |
| [9] | Bradley, A. R.; Manna, Z.; Sipma, H. B., What’s decidable about arrays?, (Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, VMCAI’06. Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, VMCAI’06, LNCS, vol. 3855 (2006), Springer), 427-442 · Zbl 1176.68116 |
| [10] | Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R., Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis, (Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’06. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’06, LNAI, vol. 4246 (2006), Springer: Springer Phnom Penh, Cambodia), 527-541 · Zbl 1165.68483 |
| [11] | Burg, J.; Lang, S.-D.; Hughes, C. E., Intelligent backtracking in CLP(R), Annals of Mathematics and Artificial Intelligence, 17, 3-4, 189-211 (1996) · Zbl 0891.68019 |
| [12] | Conchon, S.; Krstić, S., Canonization for disjoint unions of theories, (Baader, F., Proc. of the 19th International Conference on Automated Deduction. Proc. of the 19th International Conference on Automated Deduction, CADE’03. Proc. of the 19th International Conference on Automated Deduction. Proc. of the 19th International Conference on Automated Deduction, CADE’03, LNCS, vol. 2741 (2003), Springer: Springer Miami Beach, FL, USA), 197-211 · Zbl 1278.68269 |
| [13] | Conchon, S.; Krstić, S., Strategies for combining decision procedures, (Proc. of the 9th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 9th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’03. Proc. of the 9th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 9th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’03, LNCS, vol. 2619 (2003), Springer), 537-553 · Zbl 1031.68585 |
| [14] | Cyrluk, D.; Lincoln, P.; Shankar, N., On Shostak’s decision procedure for combinations of theories, (McRobbie, M. A.; Slaney, J., Proc. of the 13th International Conference on Automated Deduction. Proc. of the 13th International Conference on Automated Deduction, CADE’96, New Brunswick, NJ. Proc. of the 13th International Conference on Automated Deduction. Proc. of the 13th International Conference on Automated Deduction, CADE’96, New Brunswick, NJ, LNAI, vol. 1104 (1996), Springer), 463-477 · Zbl 1415.03019 |
| [15] | de Moura, L.; Rueß, H.; Shankar, N.; Tinelli, C.; Ranise, S., Justifying equality, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures. PDPAR 2004. Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures. PDPAR 2004, Electronic Notes in Theoretical Computer Science (ENTCS), 125, 3, 69-85 (2005) · Zbl 1272.68353 |
| [16] | Dershowitz, N.; Jouannaud, J.-P., (Handbook of Theoretical Computer Science. Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics (1990), Elsevier and MIT Press), 244-320, (Chapter 6: Rewrite Systems) · Zbl 0900.68283 |
| [17] | Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: A theorem prover for program checking, Journal of the ACM (JACM), 52, 3, 365-473 (2005) · Zbl 1323.68462 |
| [18] | Downey, P. J.; Sethi, R.; Tarjan, R. E., Variations on the common subexpression problem, Journal of the ACM, 27, 4, 758-771 (1980) · Zbl 0458.68026 |
| [19] | Enderton, H. B., A Mathematical Introduction to Logic (1972), Ac. Press, Inc · Zbl 0298.02002 |
| [20] | Fontaine, P., 2004. Techniques for Verification of Concurrent Systems with Invariants. Ph.D. Thesis, Université de Liège; Fontaine, P., 2004. Techniques for Verification of Concurrent Systems with Invariants. Ph.D. Thesis, Université de Liège |
| [21] | Fontaine, P.; Marion, J.-Y.; Merz, S.; Nieto, L. P.; Tiu, A., Expressiveness + Automation + Soundness: Towards combining SMT solvers and interactive proof assistants, (12th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2006). 12th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (2006), LNCS, vol. 3920 (2006)), 167-181 · Zbl 1180.68240 |
| [22] | Ganzinger, H., Shostak light, (Voronkov, A., Proc. of the 18th International Conference on Automated Deduction. Proc. of the 18th International Conference on Automated Deduction, CADE’02. Proc. of the 18th International Conference on Automated Deduction. Proc. of the 18th International Conference on Automated Deduction, CADE’02, LNCS, vol. 2392 (2002), Springer), 332-346 · Zbl 1072.68572 |
| [23] | Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Decision procedures for extensions of the theory of arrays, Annals of Mathematics and Artificial Intelligence, 50, 3-4, 231-254 (2007) · Zbl 1125.68115 |
| [24] | Ghilardi, S.; Nicolini, E.; Zucchelli, D., A comprehensive combination framework, ACM Transactions on Computational Logic, 9, 2, 1-54 (2008) · Zbl 1407.03011 |
| [25] | Kapur, D., Shostak’s congruence closure as completion, (Proc. of Rewriting Techniques and Applications. Proc. of Rewriting Techniques and Applications, 8th International Conference, RTA’97, Sitges, Spain, June 2-5. Proc. of Rewriting Techniques and Applications. Proc. of Rewriting Techniques and Applications, 8th International Conference, RTA’97, Sitges, Spain, June 2-5, LNCS, vol. 1232 (1997), Springer), 23-37 · Zbl 1379.68196 |
| [26] | Kapur, D., A rewrite rule based framework for combining decision procedures, (Proc. of the 4th Int. Workshop on Frontiers of Combining Systems. Proc. of the 4th Int. Workshop on Frontiers of Combining Systems, FroCos’02. Proc. of the 4th Int. Workshop on Frontiers of Combining Systems. Proc. of the 4th Int. Workshop on Frontiers of Combining Systems, FroCos’02, LNCS, vol. 2309 (2002), Springer), 87-102 · Zbl 1057.68679 |
| [27] | Kirchner, H.; Ranise, S.; Ringeissen, C.; Tran, D.-K., On superposition-based satisfiability procedures and their combination, (Proc. of Second International Colloquium on Theoretical Aspects of Computing. Proc. of Second International Colloquium on Theoretical Aspects of Computing, ICTAC’05, Hanoi, Vietnam. Proc. of Second International Colloquium on Theoretical Aspects of Computing. Proc. of Second International Colloquium on Theoretical Aspects of Computing, ICTAC’05, Hanoi, Vietnam, LNCS, vol. 3722 (2005), Springer), 594-608 · Zbl 1169.68509 |
| [28] | Kirchner, H.; Ranise, S.; Ringeissen, C.; Tran, D.-K., Automatic combinability of rewriting-based satisfiability procedures, (Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’06. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’06, LNAI, vol. 4246 (2006), Springer: Springer Phnom Penh, Cambodia), 542-556 · Zbl 1165.68490 |
| [29] | Manna, Z.; Zarba, C. G., Combining decision procedures, (Formal Methods at the Cross Roads: From Panacea to Foundational Support. Formal Methods at the Cross Roads: From Panacea to Foundational Support, LNCS, vol. 2757 (2003), Springer), 381-422 · Zbl 1274.68078 |
| [30] | Marché, C., Normalized rewriting: An alternative to rewriting modulo a set of equations, Journal of Symbolic Computation, 21, 3, 253-288 (1996) · Zbl 0859.68050 |
| [31] | Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Transations on Programming Languages and Systems, 1, 2, 245-257 (1979) · Zbl 0452.68013 |
| [32] | Nieuwenhuis, R.; Oliveras, A., Proof-producing congruence closure, (Proc. of the 16th International Conference on Rewriting Techniques and Applications. Proc. of the 16th International Conference on Rewriting Techniques and Applications, RTA’05, Nara, Japan. Proc. of the 16th International Conference on Rewriting Techniques and Applications. Proc. of the 16th International Conference on Rewriting Techniques and Applications, RTA’05, Nara, Japan, LNCS, vol. 3467 (2005), Springer), 453-468 · Zbl 1078.68661 |
| [33] | Nieuwenhuis, R.; Rubio, A., Paramodulation-based theorem proving, (Robinson, A.; Voronkov, A., Hand. of Automated Reasoning (2001), Elsevier and MIT Press), 371-443 · Zbl 0997.03012 |
| [34] | Nipkow, T., Combining matching algorithms: The regular case, Journal of Symbolic Computation, 12, 633-653 (1991) · Zbl 0767.68069 |
| [35] | Ranise, S.; Ringeissen, C.; Tran, D.-K., Nelson-Oppen, Shostak and the Extended Canonizer: A family picture with a newborn, (Proc. of First International Colloquium on Theoretical Aspects of Computing. Proc. of First International Colloquium on Theoretical Aspects of Computing, ICTAC’04, Guiyang, China. Proc. of First International Colloquium on Theoretical Aspects of Computing. Proc. of First International Colloquium on Theoretical Aspects of Computing, ICTAC’04, Guiyang, China, LNCS, vol. 3407 (2004), Springer), 372-386 · Zbl 1108.68574 |
| [36] | Ranise, S.; Ringeissen, C.; Tran, D.-K., Combining proof-producing decision procedures, (Proc. of the 6th Int. Symposium on Frontiers of Combining Systems. Proc. of the 6th Int. Symposium on Frontiers of Combining Systems, FroCos’07, Liverpool, UK. Proc. of the 6th Int. Symposium on Frontiers of Combining Systems. Proc. of the 6th Int. Symposium on Frontiers of Combining Systems, FroCos’07, Liverpool, UK, LNAI, vol. 4720 (2007)), 237-251 · Zbl 1148.68467 |
| [37] | Rueß, H.; Shankar, N., Deconstructing Shostak, (Proc. of the 16th Annual IEEE Symposium on Logic in Computer Science. Proc. of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS’01, Boston, Massachusetts, USA (2001), IEEE Computer Society), 19-28 |
| [38] | Rueß, H.; Shankar, N., Combining Shostak theories, (Tison, S., Proc. of the 13th International Conference on Rewriting Techniques and Applications, Copenhagen, Denmark. Proc. of the 13th International Conference on Rewriting Techniques and Applications, Copenhagen, Denmark, LNCS, vol. 2378 (2002), Springer), 1-18 · Zbl 1045.03015 |
| [39] | Rueß, H., Shankar, N., 2004. Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International; Rueß, H., Shankar, N., 2004. Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International |
| [40] | Sebastiani, R., Lazy satisfiability modulo theories, Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 3, 141-224 (2007) · Zbl 1145.68501 |
| [41] | Shostak, R. E., Deciding combinations of theories, Journal of the ACM, 31, 1-12 (1984) · Zbl 0629.68089 |
| [42] | Stump, A.; Tang, L.-Y., The algebra of equality proofs, (Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA). Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA), LNCS, vol. 3467 (2005), Springer), 469-483 · Zbl 1078.68740 |
| [43] | Tarjan, R. E., Efficiency of a good but not linear set union algorithm, Journal of the ACM, 22, 2, 215-225 (1975) · Zbl 0307.68029 |
| [44] | Tinelli, C.; Ringeissen, C., Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Computer Science, 290, 1, 291-353 (2003) · Zbl 1018.68033 |
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.
