Answering for first-order logic, where you have proof by negation, formally this goes something like this:
Given any sentence P in First Order Logic (atomic or complexily composed) there is another sentence NOT P (or ~P). This sentence is true only and only if P is false.
Once u commit yourself to the truth of ~P this is tantamount to committing yourself to the falsity of P.
Why would you do this? Well sometimes the negation of statements is less complex, yet equivalent so you'd want to use a less complex statement. Also with negation elimination/introduction one can 'undress' the First Order sentence, to it's atomic parts.
'Undressing' the formulas goes a great way in providing a formal proof of the sentence.
For a great introduction into first order logic and a playfull approach to negation, try to get your hands on Tarski's World.
My new guess is that in order to test for a contradiction you
A great way to test for contradictions in statements is to prove the statement holds a contradictio in terminis in its parts.
So if the sentence is like: -A && B --> (C || D) && E you try by using logical rules (such as modus ponens) to get something like (~A && A). If (~A && A) can be derived from the First order logic sentence you have proven the statement to hold contradiction.
The tautology rule is an essential rule in first order logic. It simply says for every statement A you are allowed to posit A --> A (and A --> A --> A etc.)
So you are not testing for a tautology, you are even free to introduce them, so you can 'undress' the sentence further. A tautology does not change the truth value.
Also I don't remember using truth trees in first order logic, but for semantics and maybe lambda calculus. Using truth tables will make logical equivalence visable in a flash.