FOM: Refutation Theorem Proving and Natural Deduction?

[Arnon Avron]

> In refutation theorem proving we produce a tree showing that a
> contradition can be produced while in natural deduction we produce a
> tree that the conclusion follows from the hypotheses. 
> 
> Is there any formal connection between the two trees so that one can
> be converted to the other (regardless of how hard that might be)?

My paper "Gentzen-Type Systems, Resolution and Tableaux" (Journal of
Automated Reasoning 10,  265-281, 1993),  is devoted to explaining
the deep connections between Gentzen-type systems,
tableaux and resolution in the classical case.
We show there that both resolution and tableaux (the "refutation"
methods) are based on attempts to exploit the power of 
cut-elimination theorems in Gentzen-type calculi (which are,
in turn, closely connected to Normalization theorems in natural deduction).


Arnon Avron






----------------------------------------------------------------
                                | +972-3-640-6352   Office
Prof. Arnon Avron               | +972-3-640-8040   secretary
School of Computer Science      | +972-3-640-9357   Fax
Tel Aviv University             | +972-3-641-0043   Home
Tel Aviv, 69978                 |-------------------------------
ISRAEL                          | email: aa at math.tau.ac.il
                                | http://www.math.tau.ac.il/~aa/
----------------------------------------------------------------