Simulating the DPLL(T ) procedure in a sequent calculus with focusing - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2012

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

Résumé

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.
Fichier principal
Vignette du fichier
MainHal.pdf (220.91 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00690392 , version 1 (23-04-2012)

Identifiants

  • HAL Id : hal-00690392 , version 1

Citer

Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi. Simulating the DPLL(T ) procedure in a sequent calculus with focusing. 2012. ⟨hal-00690392⟩
353 Consultations
113 Téléchargements

Partager

Gmail Facebook X LinkedIn More