A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus

International audienceWe describe how the Davis-Putnam-Logemann-Loveland proced- ure DPLL is bisimilar to the goal-directed proof-search mechanism described by a standard but carefully chosen sequent calculus. We thus relate a procedure described as a transition system on states to the gradual completion of incomplete proof-trees. For this we use a focused sequent calculus for polarised clas- sical logic, for which we allow analytic cuts. The focusing mech- anisms, together with an appropriate management of polarities, then allows the bisimulation to hold: The class of sequent calculus proofs that are the images of the DPLL runs finishing on UNSAT, is identified with a simple criterion involving polarities. We actually provide those results for a version DPLL(T ) of the procedure that is parameterised by a background theory T for which we can decide whether conjunctions of literals are con- sistent. This procedure is used for Satisfiability Modulo Theor- ies (SMT) generalising propositional SAT. For this, we extend the standard focused sequent calculus for propositional logic in the same way DPLL(T ) extends DPLL: with the ability to call the de- cision procedure for T . DPLL(T ) is implemented as a plugin for P SYCHE, a proof- search engine for this sequent calculus, to provide a sequent- calculus based SMT-solver