*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.