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