Combining Multisets with Integers
- 292 Downloads
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.
- 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.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.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