DPLL(Γ+T) and decision procedures with speculative inferences

DPLL(Γ+T) is a theorem-proving method that integrates tightly a superposition-based first-order engine, the parameter Γ, in a DPLL(T) based SMT-solver, in such a way that each does what is best at. Γ deals with non-ground clauses and uninterpreted symbols, while DPLL(T) deals 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. DPLL(Γ+T) is refutationally complete, and combines both built-in and axiomatized theories. It allows speculative inferences to induce termination on satisfiable inputs and obtain decision procedures for several theories, including axiomatizations of type systems relevant to software verification:



Maria Paola Bonacina