Simulating the DPLL(T ) procedure in a sequent calculus with focusing

Mahfuza Farooque 1, * Stéphane Lengrand 1, 2, * Assia Mahboubi 3, 1, 4, *
* 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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : This paper gives an abstract description of decision procedures for Satisfiability Modulo Theory (SMT) as proof search procedures in a sequent calculus with polarities and focusing. In particular, we show how to simulate the execution of standard techniques based on the Davis-Putnam- Logemann-Loveland (DPLL) procedure modulo theory as the gradual construction of a proof tree in sequent calculus. The construction mimicking a run of DPLL-modulo-Theory can be obtained by a meta-logical control on the proof-search in sequent calculus. This control is provided by polarities and focusing features, which there- fore narrow the corresponding search space in a sense we discuss. This simulation can also account for backjumping and learning steps, which correspond to the use of general cuts in sequent calculus.
Type de document :
Pré-publication, Document de travail
2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00690392
Contributeur : Assia Mahboubi <>
Soumis le : lundi 23 avril 2012 - 13:23:46
Dernière modification le : vendredi 10 février 2017 - 01:12:56
Document(s) archivé(s) le : lundi 26 novembre 2012 - 15:35:27

Fichier

MainHal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00690392, version 1

Collections

Citation

Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi. Simulating the DPLL(T ) procedure in a sequent calculus with focusing. 2012. <hal-00690392>

Partager

Métriques

Consultations de
la notice

387

Téléchargements du document

120