1
$\begingroup$

I'm working through some refutation proof questions for propositional logic, and I've come across the following question:

Show that the following formula is a tautology by negating it and then using refutation $$(P\ \land\ (Q\ \Rightarrow\ R))\ \Rightarrow\ ((S\ \lor\ P)\ \land\ (\neg R\ \Rightarrow\ \neg Q))$$

What I understand is I need to negate the entire formula and then convert it into CNF before performing the resolution/refutation proof. What I'm stuck on is the negation and convert to CNF part. Here's what I did:

Eliminate $\Rightarrow$:

$$(P\ \land\ (\neg Q \lor\ R))\ \Rightarrow\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$

$$\neg(P\ \land\ (\neg Q \lor\ R))\ \lor\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$

Now perform the negation step:

$$\neg(\neg(P\ \land\ (\neg Q \lor\ R))\ \lor\ ((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q)))$$

Demorgans to push the negation into the formula:

$$\neg\neg(P\ \land\ (\neg Q \lor\ R))\ \land\ \neg((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$

$$(P\ \land\ (\neg Q \lor\ R))\ \land\ \neg((S\ \lor\ P)\ \land\ (R\ \lor\ \neg Q))$$

$$(P\ \land\ (\neg Q \lor\ R))\ \land\ (\neg(S\ \lor\ P)\ \lor\ \neg(R\ \lor\ \neg Q))$$

$$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \land\ \neg P)\ \lor\ (\neg R\ \land\ Q))$$

And this is where I get stuck. I'm not sure how to proceed from here, because of that term on the right of the middle $\land$.

How do I proceed to convert this into CNF?

$\endgroup$
2
  • $\begingroup$ You should now use the distributive laws for AND and OR to massage both sides of the main connective into CNF. $\endgroup$
    – MonadBoy
    Commented Aug 28, 2016 at 12:00
  • $\begingroup$ @A.Sh are there distributive laws for formulas involving four propositional letters? $\endgroup$
    – PythonNewb
    Commented Aug 28, 2016 at 12:42

1 Answer 1

1
$\begingroup$

In these situations you need to you the distributivity laws, in your case you should proceed using

$$(a\wedge b)\vee c \leftrightarrow (a\vee c)\wedge (a\vee b), $$

where $$c:=(\neg R\wedge Q).$$

So the complete solution is as follows: $$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \land\ \neg P)\ \lor\ (\neg R\ \land\ Q))$$ $$(P\ \land\ (\neg Q \lor\ R))\ \land\ ((\neg S\ \vee\ \neg R)\ \wedge\ (\neg S\ \vee\ Q)\ \wedge (\neg P\ \vee \neg R)\ \wedge (\neg P\vee Q))$$

To satisfy this formula it must be the case $v(P)=1$, then we must have $v(R)=0$ and $v(Q)=1$, therefore this valuation cannot satisfy the clause $\neg Q \vee R$.

Resolution: You can (using resolution) infer $\{Q,\neg R\}$ applying $P$ to $\neg P\vee Q$ and $\neg P\vee\neg R$. Finally $\{Q,\neg R\}$ and $\neg Q\vee R$ gives the set $\{\neg R,R\}$, which implies the formula cannnot be satisfiable.

Comment: If you want to show that a formula is tautology, I would not negate the original formula, just transform it into conjunctive normal form. The formula is then a tautology if and only if every every clause of the CNF contains both $A$ and $\neg A$ for some atom $A$.

Proof of the last claim: from right to left: consider any valuation $v$ then it obviously must satisfy every clause, because it contains some $A$ and $\neg A$. On the other hand if you have some clause where for every atom $A$ at least on of $A$ and $\neg A$ is not in the clause. It is enough to define $v(A)=0$ iff $A$ is in the clause. It easily follows that vv does not satisfy the clause and hence the whole formula. QED

$\endgroup$
7
  • $\begingroup$ Using this I got $P\ \land\ (\neg Q\ \lor\ R)\ \land\ (\neg S\ \lor\ \neg R\ \lor\ Q)\ \land\ (\neg S\ \lor\ \neg P)$, but I don't think this is correct, because this formula cannot show that the original is a tautology $\endgroup$
    – PythonNewb
    Commented Aug 28, 2016 at 12:52
  • $\begingroup$ Okay, I've fixed that issue, and now I got $P\ \land\ (\neg Q\ \lor\ R)\ \land\ (\neg S\ \lor\ \neg R)\ \land\ (\neg S\ \lor\ Q)\ \land\ (\neg S\ \lor\ P)$, which can still not prove that the original is a tautology $\endgroup$
    – PythonNewb
    Commented Aug 28, 2016 at 13:10
  • $\begingroup$ "The formula is then a tautology if and only if every every clause of the CNF contains both $A$ and $\neg A$ for some atom $A$." Can you please expand on this? It is very interesting $\endgroup$
    – PythonNewb
    Commented Aug 28, 2016 at 13:50
  • $\begingroup$ @PythonNewb: Do you still have some doubts, or is it ok now? $\endgroup$
    – Gur Ismael
    Commented Aug 28, 2016 at 17:43
  • $\begingroup$ I think understand now, but there is still no way to perform the resolution method on your CNF formula, which is throwing me off $\endgroup$
    – PythonNewb
    Commented Aug 29, 2016 at 1:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .