# In the Resolution equivalence ($\neg A \implies B, B \implies C \models \neg A \implies C$) must $A$ be negated?

The sheet of equivalences given to us in class provides the the equivalences

\begin{array}{|c|c|c|} \hline \text{Resolution} & A \vee B, \neg B \vee C \models A \vee C & \neg A \implies B, B \implies C \models \neg A \implies C \\ \hline \end{array}

I noticed that the $A$ is negated. Is this necessary for proper Resolution? Or is this just an example that $A$ can be negated?

To me it makes logical sense that $A \implies B, B \implies C \models A \implies C$, but being somewhat new to the subject matter I would like to ensure that $\neg A$ is not necessary for Resolution.

The former statement is just the fact that if you start with $A\vee B$ and turn it into an implication you find $\neg A\implies B$.
• Ahh so the sheet itself was just trying to be consistent within that example of Resolution, between the left and right sides? // Though by "The answer is yes" you mean in the example I have, I guess my exact question was "For every usage of Resolution must the $A$ be negated"? Feb 26, 2017 at 20:01