logiccnf

Proposition Logic : CNF Conversion


I'm trying to solve a simple exercise in which I have to convert a propositional sentence in CNF :

This is the sentence : P => (Q <=> R)

According to the resolution rule the first thing I did is to eliminate the <=> symbol in this way :

P => (Q <=> R) ---> P => (Q V R) /\ (R V Q)

Then I removed the => symbol :

P => (Q V R) /\ (R V Q) ------> ¬P V (Q V R) /\ (R V Q)

So my solution is : (¬P V Q V R) /\ (¬P V R V Q)

While the right one is : (¬P V ¬Q V R) /\ (¬P V ¬R V Q)

Can anyone help me to understand where I get wrong ?


Solution

  • StackOverflow is intended for programming questions, which rules this question off-topic. But since I've already typed that much let me add that your first step ...

    P => (Q <=> R) ---> P => (Q V R) ^ (R V Q)
    

    is incorrect.

    You know that Q<=>R means by definition (Q=>R)^(R=>Q), right? So replacing that is the first step. Then you can use the equivalences (Q=>R) ---> (~QvR) and (R=>Q) ---> (~RvQ).

    Putting that together you should get ...

    P => (Q <=> R) ---> P => (~Q V R) ^ (~R V Q)
    

    I think you can work out the rest.