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

Issue title: On the Italian Conference on Computational Logic: CILC 2009

Article type: Research Article

Authors: Nicolini, Enrica | Ringeissen, Christophe | Rusinowitch, Michael

Affiliations: LORIA-INRIA Nancy Grand Est, France. FirstName.LastName@loria.fr

Abstract: 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.

Keywords: Satisfiability Procedure, Combination, Equational Reasoning, Union of Non-Disjoint Theories, Integer Offsets

DOI: 10.3233/FI-2010-362

Journal: Fundamenta Informaticae, vol. 105, no. 1-2, pp. 163-187, 2010