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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/hal-00854426
Contributor : Assia Mahboubi <>
Submitted on : Tuesday, August 27, 2013 - 10:57:20 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on: Thursday, April 6, 2017 - 9:18:54 AM

File

DPLL-LK.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

462

Files downloads

259