I'm studying for my propositional logic exam and I came across this. I do not understand what this means. I know what a resolvent of two clauses are, I just don't know what I have to do. I do not want the answer to the exercise. I just want to understand what this means so I can be able to answer it on my own. If you can also give me an example problem or any other resources on this topic that will be extremely helpful. Thank you for your help!

Res(f) problem

  • $\begingroup$ Do you know what is the resolvent of two cluases ? e.g. of $\{ \lnot A, C \}$ and $\{ \lnot C \}$ ? $\endgroup$ Commented Feb 19, 2017 at 20:38
  • $\begingroup$ Thus $Res(F)$ is the set of clauses obtained adding to the "initial" set $F$ all possible resolvents obtained from couples of clauses of $F$. $\endgroup$ Commented Feb 19, 2017 at 20:39
  • $\begingroup$ @MauroALLEGRANZA Yes the resolvent will [¬A]. $\endgroup$
    – name
    Commented Feb 19, 2017 at 20:41
  • $\begingroup$ Correct. Then write $F$ plus all the resolvents... $\endgroup$ Commented Feb 19, 2017 at 20:41
  • $\begingroup$ @MauroALLEGRANZA So, I am supposed to get all resolvents of F and then add them as clauses to F? So if my F is {{¬A,C},{¬C}} then my Res(f) will be {{¬A,C},{¬C},[¬A]}? $\endgroup$
    – name
    Commented Feb 19, 2017 at 20:46


You must log in to answer this question.

Browse other questions tagged .