Predicate Logic - negating the conclusion to prove logical consequence? In Predicate Logic, if you want to prove the logical consequence using the method of resolution, do you ALWAYS start off by negating the conclusion?
The method works in the same way as proofs by contradiction. Suppose you have a set of assumptions $A$ and you want to prove that formula $\phi$ is a logical consequence of the formulas in $A$. One of the ways to do this is as follows.


Put the negation of $\phi$ in your assumptions. So, now $A' = A\cup\{\neg\phi\}$
Show that $A'$ is inconsistent. Here, this means to consecutively apply the resolution step on (appropriately chosen) formulas of $A'$, until a contradiction $(T\to F)$ is reached.


Classical logic tells you that, if (a) the initial set of assumptions $A$ is consistent and (b) $A\cup\{\neg\phi\}$ is inconsistent, then $A\cup\{\phi\}$ is consistent and you can say that $\phi$ is a logical consequence of $A$. So, if steps (1) and (2) succeed, then $\phi$ is a logical consequence of $A$.

If you don't negate the goal when you put it in the set of assumptions and  if you manage to show that $A\cup\{\phi\}$ is inconsistent, then $A\cup\{\neg\phi\}$ is consistent and therefore $\neg\phi$ is a logical consequence of $A$.