Combining Sets with Integers
We present a decision procedure for a constraint language combining stratified sets of ur-elements with integers in the presence of a cardinality operator. Our decision procedure is an extension of the Nelson-Oppen combination method specifically tailored to the combination domain of sets, integers, and ur-elements.
KeywordsVenn Diagram Disjunctive Normal Form Separate Form Constraint Language Combination Domain
Unable to display preview. Download preview PDF.
- 1.Domenico Cantone and Vincenzo Cutello. A decision procedure for set-theoretic formulae involving rank and cardinality comparison. In A. Bertoni, C. Böhm,and P. Miglioli,eds., Proceedings of the 3rd Italian Conference on Theoretical Computer Science,pages 150–163. World Scientific,1989.Google Scholar
- 2.Domenico Cantone, Vincenzo Cutello, and Jacob T. Schwartz. Decision problems for Tarski’s and Presburger arithmetics extended with sets. In Proceedings of the fourth Computer Science Logic Workshop, volume 533 of Lecture Notes in Computer Science,pages 95–109. Springer,1990.Google Scholar
- 3.Domenico Cantone and Calogero G. Zarba. A tableau calculus for integrating firstorder reasoning with elementary set theory reasoning. In Roy Dyckhoff, ed., Automated Reasoning with Analytic Tableaux and Related Methods, volume 1847 of Lecture Notes in Artificial Intelligence, pages 143–159. Springer,2000.Google Scholar
- 6.Cesare Tinelli and Mehdi T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Franz Baader and Klaus U. Schulz,eds., Frontiers of Combining Systems, volume 3 of Applied Logic Series,pages 103–120. Kluwer Academic Publishers, 1996.Google Scholar
- 7.John Venn. On the diagrammatic and mechanical representation of propositions and reasonings. The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, 9(59):1–18, 1880.Google Scholar
- 8.Calogero G. Zarba. Combining lists with integers. In Rajeev Gorè, Alexander Leitsch, and Tobias Nipkow, eds., International Joint Conference on Automated Reasoning (Short Papers), Technical Report DII 11/01, pages 170–179. University of Siena, Italy, 2001.Google Scholar