Journal article
Combining Non-Stably Infinite Theories
Electronic notes in theoretical computer science, Vol.86(1), pp.35-48
05/2003
DOI: 10.1016/S1571-0661(04)80651-0
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. 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 provide a new combination method that can combine any theory that is not stably infinite with another theory, provided that the latter is what we call a shiny theory. Examples of shiny theories include the theory of equality, the theory of partial orders, and the theory of total orders.
An interesting consequence of our results is that any decision procedure for the satisfiability of quantifier-free Σ-formulae in a Σ-theory T can always be extended to accept inputs over an arbitrary signature Ω ⊇ Σ.
Details
- Title: Subtitle
- Combining Non-Stably Infinite Theories
- Creators
- Cesare Tinelli - University of IowaCalogero G Zarba - Stanford University
- Resource Type
- Journal article
- Publication Details
- Electronic notes in theoretical computer science, Vol.86(1), pp.35-48
- DOI
- 10.1016/S1571-0661(04)80651-0
- ISSN
- 1571-0661
- eISSN
- 1571-0661
- Publisher
- Elsevier B.V
- Language
- English
- Date published
- 05/2003
- Academic Unit
- Computer Science
- Record Identifier
- 9984259499402771
Metrics
19 Record Views