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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.