Theory Combination: Beyond Equality Sharing

Maria Paola Bonacina 1 Pascal Fontaine 2 Christophe Ringeissen 3 Cesare Tinelli 4
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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).
Document type :
Book sections
Complete list of metadatas

Cited literature [135 references]  Display  Hide  Download

https://hal.inria.fr/hal-02194001
Contributor : Pascal Fontaine <>
Submitted on : Thursday, July 25, 2019 - 9:54:09 AM
Last modification on : Monday, September 9, 2019 - 11:11:10 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02194001, version 1

Collections

Citation

Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli. Theory Combination: Beyond Equality Sharing. Carsten Lutz; Uli Sattler; Cesare Tinelli; Anni-Yasmin Turhan; Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.57-89, 2019, Theoretical Computer Science and General Issues, 978-3-030-22101-0. ⟨hal-02194001⟩

Share

Metrics

Record views

36

Files downloads

245