  In this paper we relate different formulations of the DPLL(T) procedure. The
first formulation is based on a system of rewrite rules, which we denote
DPLL(T). The second formulation is an inference system of, which we denote
LKDPLL(T). The third formulation is the application of a standard proof-search
mechanism in a sequent calculus LKp(T) introduced here. We formalise an
encoding from DPLL(T) to LKDPLL(T) that was, to our knowledge, never explicitly
given and, in the case where DPLL(T) is extended with backjumping and Lemma
learning, never even implicitly given. We also formalise an encoding from
LKDPLL(T) to LKp(T), building on Ivan Gazeau's previous work: we extend his
work in that we handle the "-modulo-Theory" aspect of SAT-modulo-theory, by
extending the sequent calculus to allow calls to a theory solver (seen as a
blackbox). We also extend his work in that we handle advanced features of DPLL
such as backjumping and Lemma learning, etc. Finally, we re fine the approach
by starting to formalise quantitative aspects of the simulations: the
complexity is preserved (number of steps to build complete proofs). Other
aspects remain to be formalised (non-determinism of the search / width of
search space).
