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:
While a tableau (with all the branches rejected) is the following:
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?
