FOM: Refutation Theorem Proving and Natural Deduction?

[Steve Stevenson]

Good morning,

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

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?

best,
steve