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

Question

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.

Answer 1

The answer is yes. But the departure point is slightly different. Here it is:

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

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$.