A theorem proving method with DPLL(T) and superposition: DPLL(Γ+T)
The approach of
decision procedures by stages
applied the superposition-based first-order engine as a pre-processor for the SMT-solver,
somewhat in the spirit of using completion to get a saturated set.
Like theorem proving profited from
viewing completion as a theorem prover,
rather than as a generator of saturated sets,
and continuing the work on
rewrite-based satisfiability procedures,
the next phase was to design a theorem proving method that integrates first-order engine and SMT-solver:
- 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.
- Maria Paola Bonacina, Christopher A. Lynch and Leonardo de Moura.
On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving.
In Proceedings of the Twenty-second 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).
The resulting inference system DPLL(Γ+T),
implemented in the Z3(SP) prototype,
is refutationally complete,
uses
variable inactivity,
to combine built-in and axiomatized theories,
and allows speculative inferences to induce termination on satisfiable inputs.
This approach yields decision procedures for axiomatizations
of type systems relevant to software verification.
Maria Paola Bonacina