Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid?
And given that the latter problem asks for less information (e.g. no need for a "counterexample" in case the formula is invalid), is it possible to solve it more efficiently than standard SAT solving?
