Book chapter
Theory Combination: Beyond Equality Sharing
Description Logic, Theory Combination, and All That, pp.57-89
Lecture Notes in Computer Science, Springer International Publishing
06/01/2019
DOI: 10.1007/978-3-030-22102-7_3
Abstract
Satisfiability is the problem of deciding whether a formula has a model. Although it is not even semidecidable in first-order logic, it is decidable in some first-order theories or fragments thereof (e.g., the quantifier-free fragment). Satisfiability modulo a theory is the problem of determining whether a quantifier-free formula admits a model that is a model of a given theory. If the formula mixes theories, the considered theory is their union, and combination of theories is the problem of combining decision procedures for the individual theories to get one for their union. A standard solution is the equality-sharing method by Nelson and Oppen, which requires the theories to be disjoint and stably infinite. This paper surveys selected approaches to the problem of reasoning in the union of disjoint theories, that aim at going beyond equality sharing, including: asymmetric extensions of equality sharing, where some theories are unrestricted, while others must satisfy stronger requirements than stable infiniteness; superposition-based decision procedures; and current work on conflict-driven satisfiability (CDSAT).
Details
- Title: Subtitle
- Theory Combination: Beyond Equality Sharing
- Creators
- Maria Paola Bonacina - University of VeronaPascal Fontaine - Modeling and Verification of Distributed Algorithms and SystemsChristophe Ringeissen - Université de LorraineCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Description Logic, Theory Combination, and All That, pp.57-89
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-22102-7_3
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 06/01/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259501402771
Metrics
23 Record Views