Skip to Main content Skip to Navigation
Reports

A model-constructing framework for theory combination

Abstract : This report presents a model-constructing satisfiability calculus (MCSAT) for (quantifier-free) first-order logic modulo a generic combination of disjoint theories. We determine the requirements that the theories and their decision procedures need to satisfy for an MC-SAT combination, thus generalizing the MCSAT calculus of De Moura and Jovanović, that was introduced for one generic theory and extended to a combination of specific disjoint theories. We prove soundness, completeness, and termination of the generalized calculus.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-01425305
Contributor : Stéphane Graham-Lengrand <>
Submitted on : Tuesday, January 3, 2017 - 2:53:52 PM
Last modification on : Thursday, March 5, 2020 - 6:34:07 PM

Identifiers

  • HAL Id : hal-01425305, version 1

Collections

Citation

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. A model-constructing framework for theory combination. [Research Report] RR-99/2016, Universita degli Studi di Verona. 2016. ⟨hal-01425305⟩

Share

Metrics

Record views

500