This report presents a conflict-driven satisfiability inference system (CDSAT) 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 a CDSAT combination, generalizing the MCSAT system of De Moura and Jovanovic, that was introduced for one generic theory and extended to a combination of specific disjoint theories. We prove soundness, completeness, and termination of CDSAT.
A model-constructing framework for theory combination
BONACINA, Maria Paola;
2016-01-01
Abstract
This report presents a conflict-driven satisfiability inference system (CDSAT) 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 a CDSAT combination, generalizing the MCSAT system of De Moura and Jovanovic, that was introduced for one generic theory and extended to a combination of specific disjoint theories. We prove soundness, completeness, and termination of CDSAT.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
