## CDCL(Γ+T) and decision procedures with speculative inferences

CDCL(Γ+*T*) is a reasoning method that integrates tightly a
superposition-based first-order inference system, the parameter Γ, in a
CDCL(*T*) based SMT-solver.
The original name is DPLL((Γ+*T*), but if one uses CDCL(*T*) in place of
DPLL(*T*), as it has become common, then one should say CDCL(Γ+*T*).
CDCL(Γ+*T*) is presented as a transition system, where the Γ-transitions
deal with non-ground clauses and uninterpreted symbols, while the CDCL(*T*) transitions
deal with ground clauses and interpreted symbols; both see unit ground clauses made of
uninterpreted symbols. They communicate through the *trail* that represents the
candidate model built by the SMT-solver, as Γ uses literals in the trail as premises.
Thus, the Γ-inferences are *model-driven*. CDCL(Γ+*T*) is
refutationally complete, and combines both built-in and axiomatized theories.
It allows *speculative inferences* to induce termination on satisfiable inputs and
is a *decision procedure* for several theories, including axiomatizations of
*type systems* relevant to software verification:

- Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
On
deciding satisfiability by theorem proving with speculative inferences.
*Journal of Automated Reasoning*, 47(2):161-189, August 2011; DOI: 10.1007/s10817-010-9213-y
(presented in part at the Workshop on Automated Deduction and its Application to Mathematics (ADAM), Department of Computer Science, University of New Mexico, Albuquerque, New Mexico, USA, June 2013:
Slides).

- Maria Paola Bonacina.
On theorem proving for program checking - Historical perspective and recent developments.
In
*Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP)*,
Schloss Hagenberg, Linz, Austria, July 2010. ACM Press, 1-11, 2010 (**invited talk**);
DOI: 10.1145/1836089.1836090
(©[ACM Inc.][2010]).

- Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
On
deciding satisfiability by DPLL(Γ+
*T*) and unsound theorem
proving. In *Proceedings of the 22nd International Conference on Automated Deduction
(CADE)*, Montréal, Canada, August 2009.
Springer,
Lecture Notes in Artificial Intelligence 5663, 35-50, 2009;
DOI: 10.1007/978-3-642-02959-2_3
(presented in part at the Dagstuhl
Seminar 09411 on Interaction vs. Automation: the Two Faces of Deduction,
October 2009:
Slides).

- Maria Paola Bonacina.
On
model-based reasoning: recent trends and current developments (Abstract).
In
*Proceedings of the 28th Italian Conference on Computational Logic (CILC)*, Catania, Italy,
September 2013. CEUR Proceedings 1068:9-9, 2013 (**invited talk**).

*Maria Paola Bonacina*