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, Fourier-Motzkin elimination and Groebner bases computation. | | Keywords | Satisfiability Procedure, Combination, Equational Reasoning, Union of Non-Disjoint Theories, Integer Offsets | | ISSN | 0169-2968; 1875-8681/e |
| URL |
http://content.iospress.com/articles/fundamenta-informaticae/fi105-1-2-08 |
| Language | English | | Journal | Fundam. Inform. | | Volume | 105 | | Number | 1-2 | | Pages | 163--187 | | Publisher | IOS Press, Amsterdam; Polish Mathematical Society (Polskie Towarzystwo Matematyczne - PTM), Warsaw | | Year | 2010 | | Edition | 0 | | Translation |
No | | Refereed |
No |
|
