Skip to Main content Skip to Navigation
New interface
Conference papers

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

Mahfuza Farooque 1, 2, * Stéphane Lengrand 1, 2, * Assia Mahboubi 3, * 
* Corresponding author
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Tuesday, August 27, 2013 - 10:57:20 AM
Last modification on : Friday, August 5, 2022 - 9:26:01 AM
Long-term archiving on: : Thursday, April 6, 2017 - 9:18:54 AM


Files produced by the author(s)




Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ⟨10.1145/2503887.2503892⟩. ⟨hal-00854426⟩



Record views


Files downloads