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.


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

  • $\begingroup$ 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"? $\endgroup$
    – KDecker
    Feb 26, 2017 at 20:01
  • $\begingroup$ Both are correct, it depends just from the departure assumptions. $\endgroup$
    – Maczinga
    Feb 26, 2017 at 20:03
  • $\begingroup$ Thank you! Makes sense I think! If you'd like to answer another question, I have another subject matter related question (cs.stackexchange.com/questions/70828/…) $\endgroup$
    – KDecker
    Feb 26, 2017 at 20:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.