Journal article
Combining nonstably infinite theories
Journal of automated reasoning, Vol.34(3), pp.209-238
04/01/2005
DOI: 10.1007/s10817-005-5204-9
Abstract
The Nelson-Oppen combination method combines decision procedures for first-order theories over disjoint signatures into a single decision procedure for the union theory. In order to be correct, the method requires that the component theories be stably infinite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only finite models.
In this paper, we describe two extensions of the Nelson-Oppen method that address the problem of combining theories that are not stably infinite. In our extensions, the component decision procedures exchange not only equalities between shared variables but also certain cardinality constraints.
Applications of our results include the combination of theories having only finite models, as well as the combination of nonstably infinite theories with the theory of equality, the theories of total and partial orders, and the theory of lattices with maximum and minimum.
Details
- Title: Subtitle
- Combining nonstably infinite theories
- Creators
- Cesare Tinelli - University of IowaCalogero G. Zarba - University of New Mexico
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.34(3), pp.209-238
- Publisher
- Springer Nature
- DOI
- 10.1007/s10817-005-5204-9
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Number of pages
- 30
- Language
- English
- Date published
- 04/01/2005
- Academic Unit
- Computer Science
- Record Identifier
- 9984259501902771
Metrics
14 Record Views