# using resolution rule, check if the following is a tautology

i understand how to use resolution but i get to an answer and i dont know if its ok. I need to check if the following is a tautology only using resolution rules.

(p∨q)→(q→(p∨(p∧q))

i get to the following clauses: p∨q, q, ¬p, ¬p∨¬q I dont know how to procede past that.

Also i have a second question about resolution: i want to know, what happens if i get a clause with (¬p∨p)

• You might do best to reread what the resolution rule of inference says, and look for pairs of clauses where $\phi$ and $\lnot$$\phi$ both appear within the formula. In your example $\lnot$p appears in one formula, and p appears in another. Thus, you can infer the rest of the clause without p, or $\lnot$p according to the resolution rule of inference. There's only so many clauses that you can infer here, and no clause that you can infer is the empty set here. Thus, you might list all of the clauses that can get inferred and then indicate that the empty set is not one of them. Apr 16 '20 at 0:51
• So, i get no empty set, that means is not a tautology? Also if i get an empty set it is a tautology ? (not this case) Apr 16 '20 at 1:04
• If you get an empty set, then it's a tautology. If you've deduced all possible formulas that can get deduced and there is no empty set, then it's not a tautology. Apr 16 '20 at 1:22
• Thanks!! this is very helpfull Apr 16 '20 at 1:26

Now back to your problem. You are actually quite right in that you're basically stuck: the only new clauses you can get from the ones you have are $$p \lor \neg p$$ and $$q \lor \neg q$$. Both being tautologous clauses, that does not get you anywhere. And given that you can;t get anything else, that tells you you won;t get to a contradiction. Moreover, the $$q$$ and $$\neg p$$ clauses tells you exactly the model that will make the statement False: if you set $$q$$ to True and $$p$$ to False, then you'll find that the original statement evaluates to False, and thus is not a tautology.
Finally, form the clauses that you have, you can remove the clauses $$p \lor q$$, since it is subsumed by the clause $$q$$. Likewise, you can remove the $$\neg p \lor \neg q$$ clauses since it is subsumed by $$\neg p$$. So, you are left with $$q$$ and $$\neg p$$ ... and now it is obvious that you won't get a contradiction from that!
• @Cipher not getting an empty set would suggest it is not a tautology ... but you have to be careful: You have to make sure that you have tried all possible resolutions and that there are indeed no more new clauses to be obtained. So for this to become a demonstration, you need to systematically demonstrate that there are no new clauses to be obtained. Saying "Well, I couldn;t get to en empty clause" is really not enough: maybe you weren't trying hard enough to find new clauses! :) But in this case it's clear, especially after removing the subsumed clauses and ending up with $q$ and $\neg p$. Apr 16 '20 at 13:44