Combining Sets with Integers

  • Calogero G. Zarba
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2309)


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.


Venn Diagram Disjunctive Normal Form Separate Form Constraint Language Combination Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 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
  4. 4.
    Alfredo Ferro, Eugenio G. Omodeo, and Jacob T. Scwhartz. Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions. Communications on Pure and Applied Mathematics, 33(5):599–608, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.zbMATHCrossRefGoogle Scholar
  6. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Calogero G. Zarba
    • 1
    • 2
  1. 1.Stanford UniversityStanford
  2. 2.University of CataniaCatania

Personalised recommendations