A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi · 2013
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.