Which kind of relationship is there between natural deduction refutations of a set f propositional logic assumptions, and the corresponding tableaux?

For example, consider the unsatisfiable set $\Gamma=\{p\to q, p, \neg q\}$.

A natural deduction refutation for $\Gamma$ is as follows: natural refutation

While a tableau (with all the branches rejected) is the following: tableau

Note that the refutation proof is similar to what a SAT/SMT solver would produce, while a tableau-based decision procedure would produce the tree in the second picture.

Now, which relationship is there between the two? In particular, can I recover the tableau tree from the proof, or vice versa? Is one potentially more succinct than the other? Both should carry the same information, namely that there is no assignment that satisfies the set of formulas, so they should be somewhat similar objects, but they do appear very different.

I'm not an expert in proof theory and of course these objects have been studied extensively, so maybe what I need is somewhere out there.

Which papers/books should I read on this subject?



Your Answer

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