# FOM: Refutation Theorem Proving and Natural Deduction?

Richard Zach rzach at ucalgary.ca
Mon Jun 3 12:20:41 EDT 2002

> 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/