FOM: Refutation Theorem Proving and Natural Deduction?

[Richard Zach]

 > 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)?

There are very simple connections between tableaux and sequent 
calculus/natural deduction--essentially a tableaux proof is a compressed 
  version of a sequent proof, as Allen Hazen pointed out. The situation 
is much more complicated with resolution proofs.  Here most of the 
logical structure of the proof is not in the refutation (which starts 
from logic-free clauses) itself, but in the translation of the formula 
to clause form.

For the propositional case, a good place for references is probably

The complexity of propositional proofs, by Alasdair Urquhart, Bulletin 
Symbolic logic 1 (1995) 425 - 467.
http://www.math.ucla.edu/~asl/bsl/01-toc.htm

which surveys the various results on simulations between various 
propositional proof systems, as well as Arnon's paper.

Another useful reference is perhaps
Wolfgang Bibel and Elmar Eder. Chapter 3: Methods and calculi for 
deduction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, 
Handbook of Logic in Artificial Intelligence and Logic Programming, 
Volume 1, chapter 3, pages 67-182. Oxford University Press, 1993.
http://www.cosy.sbg.ac.at/~eder/list-of-papers.html#1993-handbook-chapter3

 > All the algorithms I know for setting up the refutation search require
 > conversion to conjuntive normal form. Doesn't this require the
 > excluded middle? Doesn't that make refutation style systems impossible
 > for intuitionistic systems?

No; there are generic resolution methods which are very similar to 
classical resolution but which work for non-classical systems.  The 
simplest is perhaps signed resolution for many-valued logic: here, 
instead of two signs (negated, unnegated) you have one sign for each 
truth value, and the resolution rule is simply extended from

{A} \cup C; {~A} \cup D => C \cup D

to

{v: A} \cup C; {v':A} \cup D => C \cup D

where v \neq v'.

The inverse method due to Maslov and Mints is another refutational 
method which works for non-classical logics. Essentially, all you need 
is an analytic calculus for the logic. Tammett has developed an inverse 
method for intuitionistic logic, see his paper on

'A Resolution Theorem Prover for Intuitionistic Logic' ,
http://www.cs.chalmers.se/pub/users/tammet/

For signed resolution, see
Matthias Baaz, Christian G. Fermüller, Gernot Salzer: Automated 
Deduction for Many-Valued Logics. in: John Alan Robinson, Andrei 
Voronkov (Eds.): Handbook of Automated Reasoning, Vol 2, Elsevier and 
MIT Press 2001, pp 1355-1402

-Richard Zach
http://www.ucalgary.ca/~rzach/