Details:
Title  Combining satisfiability procedures for unions of theories with a shared counting operator.  Author(s)  Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch  Type  Article in Journal  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, FourierMotzkin elimination and Groebner bases computation.  Keywords  Satisfiability Procedure, Combination, Equational Reasoning, Union of NonDisjoint Theories, Integer Offsets  ISSN  01692968; 18758681/e 
URL 
http://content.iospress.com/articles/fundamentainformaticae/fi1051208 
Language  English  Journal  Fundam. Inform.  Volume  105  Number  12  Pages  163187  Publisher  IOS Press, Amsterdam; Polish Mathematical Society (Polskie Towarzystwo Matematyczne  PTM), Warsaw  Year  2010  Edition  0  Translation 
No  Refereed 
No 
