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$
  • $\begingroup$ You should now use the distributive laws for AND and OR to massage both sides of the main connective into CNF. $\endgroup$ – A.Sh Aug 28 '16 at 12:00
  • $\begingroup$ @A.Sh are there distributive laws for formulas involving four propositional letters? $\endgroup$ – PythonNewb Aug 28 '16 at 12:42
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$
  • $\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 Aug 28 '16 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 Aug 28 '16 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 Aug 28 '16 at 13:50
  • $\begingroup$ @PythonNewb: Do you still have some doubts, or is it ok now? $\endgroup$ – Gur Ismael Aug 28 '16 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 Aug 29 '16 at 1:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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