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, *
* Auteur correspondant
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Alberto Momigliano and Brigitte Pientka and Randy Pollack. LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice - 2013, Sep 2013, Boston, United States. ACM, 2013, 〈10.1145/2503887.2503892〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00854426
Contributeur : Assia Mahboubi <>
Soumis le : mardi 27 août 2013 - 10:57:20
Dernière modification le : jeudi 10 mai 2018 - 02:06:52
Document(s) archivé(s) le : jeudi 6 avril 2017 - 09:18:54

Fichier

DPLL-LK.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

374

Téléchargements de fichiers

143