salle A. Turing CE4
25 novembre 2013 - 11h30
A Bisimulation between DPLL(T) and a Proof-Search Strategy for the Focused Sequent Calculus
par Mahfuza Farooque de École polytechnique
Abstract: We describe how the Davis-Putnam-Logemann-Loveland procedure 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 classical logic,
for which we allow analytic cuts. The focusing mechanisms, 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 consistent. This procedure is used
for Satisfiability Modulo Theories (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 decision procedure for T.
DPLL(T) is implemented as a plugin for Psyche, a proof-search engine for
this sequent calculus, to provide a sequent-calculus based SMT-solver.
