DPLL ( T ) as a goal-directed proof-search mechanism

We describe how the Davis-Putnam-Logemann-Loveland procedure, in its version DPLL(T ) for Satisfiability Modulo Theory (SMT), can be interpreted as a proof-search mechanism for the incremental construction of a proof tree in sequent calculus. For this we use a sequent calculus with polarities and focusing and show how its meta-logical control features allow for a precise simulation of runs of DPLL(T ). This simulation also accounts for backjumping and learning steps. Finally we describe Psyche, an extensible prototype for this sequent calculus, that includes the implementation of a proof-search component based on this simulation of DPLL(T ).