Theory Combination: Beyond Equality Sharing - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2019

Theory Combination: Beyond Equality Sharing

Résumé

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).
Fichier principal
Vignette du fichier
paper.pdf (460.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02194001 , version 1 (25-07-2019)

Identifiants

  • HAL Id : hal-02194001 , version 1

Citer

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⟩
70 Consultations
208 Téléchargements

Partager

Gmail Facebook X LinkedIn More