Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleCombining satisfiability procedures for unions of theories with a shared counting operator.
Author(s) Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch
TypeArticle in Journal
AbstractWe 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.
KeywordsSatisfiability Procedure, Combination, Equational Reasoning, Union of Non-Disjoint Theories, Integer Offsets
ISSN0169-2968; 1875-8681/e
URL http://content.iospress.com/articles/fundamenta-informaticae/fi105-1-2-08
JournalFundam. Inform.
PublisherIOS Press, Amsterdam; Polish Mathematical Society (Polskie Towarzystwo Matematyczne - PTM), Warsaw
Translation No
Refereed No