Loading...
Please wait, while we are loading the content...
Similar Documents
A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
| Content Provider | ACM Digital Library |
|---|---|
| Author | Graham-Lengrand, Stéphane Mahboubi, Assia Farooque, Mahfuza |
| Abstract | We describe how the Davis-Putnam-Logemann-Loveland procedure 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 classical logic, for which we allow analytic cuts. The focusing mechanisms, 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 consistent. This procedure is used for Satisfiability Modulo Theories (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 decision procedure for T. DPLL(T) is implemented as a plugin for Psyche, a proof-search engine for this sequent calculus, to provide a sequent-calculus based SMT-solver. |
| Starting Page | 3 |
| Ending Page | 14 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781450323826 |
| DOI | 10.1145/2503887.2503892 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2013-09-23 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Polarised logic Focused sequent calculus Dpll(t) |
| Content Type | Text |
| Resource Type | Article |
