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

Mahfuza Farooque 1, * Stéphane Lengrand 1, 2, * Assia Mahboubi 3, 1, 4, *
* 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]
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00690392
Contributor : Assia Mahboubi <>
Submitted on : Monday, April 23, 2012 - 1:23:46 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Monday, November 26, 2012 - 3:35:27 PM

File

MainHal.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

603

Files downloads

164