Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator

• Autorzy: Nicolini, E. , Ringeissen, C. , Rusinowitch, M.
• Języki publikacji: EN

Abstrakty

EN

We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for the successor. A general decision procedure is obtained, by devising an appropriate calculus based on superposition. Moreover, we derive a decidability result for the combination of the considered theories for data structures and some fragments of arithmetic by applying a general combination schema for theories sharing a common subtheory. The effectiveness of the resulting algorithm is ensured by using the proposed calculus and a careful adaptation of standard methods for reasoning about arithmetic, such as Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.

Słowa kluczowe

EN

satisfiability procedure; combination; equational reasoning; union of non-disjoint teories; integer offsets

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 105, nr 1/2
• Strony: 163-187
• Opis fizyczny: Bibliogr. 32 poz.

Twórcy

autor

Nicolini, E.

autor

Ringeissen, C.

autor

Rusinowitch, M.

• INRIA Grand Est, 615 rue du Jardin Botanique, CS 20101, 54603 Villers-les-Nancy Cedex France,

Bibliografia

• [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.
• [2] Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures, Information and Computation, 183(2), 2003, 140-164.
• [3] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation, 4(3), 1994, 217-247.
• [4] Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on Demand in SAT Modulo Theories, Proc.of LPAR'06, 4246, Springer, 2006.
• [5] Bonacina, M. P., Echenim, M.: On Variable-inactivity and Polynomial T-Satisfiability Procedures, Journal of Logic and Computation, 18(1), 2008, 77-96.
• [6] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T. A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Theory Combination via Boolean Search, Information and Computation, 204(10), 2006, 1493-1525.
• [7] Bradley, A., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer, 2007.
• [8] Bryant, R. E., Lahiri, S. K., Seshia, S. A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proc. of CAV'02, 2404, Springer, 2002.
• [9] Buchberger, B.: A Theoretical Basis for the Reduction of Polynomials to Canonical Forms, ACM SIGSAM Bull., 10(3), 1976, 19-29.
• [10] Dershowitz, N., Plaisted, D.: Rewriting, in: Handbook of Automated Reasoning (A. Robinson, A. Voronkov, Eds.), vol. I, chapter 9, Elsevier Science, 2001, 535-610.
• [11] Enderton, H. B.: A Mathematical Introduction to Logic, Academic Press, New York-London, 1972.
• [12] Ghilardi, S.: Model Theoretic Methods in Combined Constraint Satisfiability, Journal of Automated Reasoning, 33(3-4), 2004, 221-249.
• [13] Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Noetherianity and Combination Problems, Proc. Of FroCoS'07, 4720, Springer, 2007.
• [14] Ghilardi, S., Nicolini, E., Zucchelli, D.: A Comprehensive Combination Framework, ACM Transactions on Computational Logic, 9(2), 2008, 1-54.
• [15] Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On Superposition-Based Satisfiability Procedures and Their Combination, Proc. of ICTAC'05, 3722, Springer, 2005.
• [16] Lassez, J.-L., Maher, M. J.: On Fourier's Algorithm for Linear Arithmetic Constraints, Journal of Automated Reasoning, 9(3), 1992, 373-379.
• [17] Lassez, J.-L., McAloon, K.: A Canonical Form for Generalized Linear Constraints, Journal of Symbolic Computation, 13(1), 1992, 1-24.
• [18] Lynch, C., Tran, D.-K.: SMELS: Satisfiability Modulo Equality with Lazy Superposition, Proc. of ATVA'08, 5311, Springer, 2008.
• [19] Manna, Z., Zarba, C. G.: Combining Decision Procedures, Formal Methods at the Cross Roads: From Panacea to Foundational Support, 2757, Springer, 2003.
• [20] Nelson, G., Oppen, D. C.: Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, 1(2), 1979, 245-257.
• [21] Nicolini, E.: Combined decision procedures for constraint satisfiability, Ph.D. Thesis, Universit`a degli Studi di Milano, 2007.
• [22] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable Extensions of Abelian Groups, Proc. Of CADE'09, 5663, Springer, 2009.
• [23] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data Structures with Arithmetic Constraints: a Non-Disjoint Combination, Proc. of FroCoS'09, 5749, Springer, 2009, Also as INRIA Report RR-6963.
• [24] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Proc. of TACAS'09, 5505, Springer, 2009, Also as INRIA Report RR-6697.
• [25] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)., Journal of the ACM, 53(6), 2006, 937-977.
• [26] Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving, in: Handbook of Automated Reasoning (A. Robinson, A. Voronkov, Eds.), vol. I, chapter 7, Elsevier Science, 2001, 371-443.
• [27] Oppen, D. C.: Reasoning About Recursively Defined Data Structures, Journal of the ACM, 27(3), 1980, 403-411.
• [28] Shostak, R. E.: Deciding Combinations of Theories, Journal of the ACM, 31, 1984, 1-12.
• [29] Tinelli, C., Ringeissen, C.: Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures, Theoretical Computer Science, 290(1), January 2003, 291-353.
• [30] Tran, D.-K., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation, Journal of Symbolic Computation, 45, 2010, 261-286, Special issue on Automated Deduction: Decidability, Complexity, Tractability.
• [31] Zarba, C. G.: A Tableau Calculus for Combining Non-disjoint Theories, Proc. of TABLEAUX'02, 2381, Springer, 2002.
• [32] Zucchelli, D.: Combination Methods for Software Verification, Ph.D. Thesis, Universit`a degli Studi di Milano and Université Henri Poincaré - Nancy 1, 2008.