Combining Multisets with Integers

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


We present a decision procedure for a constraint language combining multisets of ur-elements, the integers, and an arbitrary first-order theory T of the ur-elements. Our decision procedure is an extension of the Nelson-Oppen combination method specifically tailored to the combination domain of multisets, integers, and ur-elements.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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
  2. 2.
    Christos H. Papadimitriou. On the complexity of integer programming. Journal of the Association for Computing Machinery, 28(4):765–768, 1981.zbMATHMathSciNetGoogle Scholar
  3. 3.
    Cesare Tinelli and Mehdi T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Franz Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems, volume 3 of Applied Logic Series, pages 103–120. Kluwer Academic Publishers, 1996.Google Scholar
  4. 4.
    Calogero G. Zarba. Combining lists with integers. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, International Joint Conference on Automated Reasoning (Short Papers), Technical Report DII 11/01, pages 170–179. University of Siena, Italy, 2001.Google Scholar
  5. 5.
    Calogero G. Zarba. Combining sets with integers. In Alessandro Armando, editor, Frontiers of Combining Systems, volume 2309 of Lecture Notes in Artificial Intelligence, pages 103–116. Springer, 2002.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Calogero G. Zarba
    • 1
    • 2
  1. 1.Stanford UniversityUSA
  2. 2.University of CataniaItaly

Personalised recommendations