A model-constructing framework for theory combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar · HAL (Le Centre pour la Communication Scientifique Directe) · 2016
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.