0
$\begingroup$

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)

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$ – Doug Spoonwood Apr 16 '20 at 0:51
  • $\begingroup$ 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) $\endgroup$ – Cipher Apr 16 '20 at 1:04
  • $\begingroup$ 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. $\endgroup$ – Doug Spoonwood Apr 16 '20 at 1:22
  • $\begingroup$ Thanks!! this is very helpfull $\endgroup$ – Cipher Apr 16 '20 at 1:26
1
$\begingroup$

First, a clause with an atomic proposition and its negation both in it is called a tautologous clause. That makes sense, since the statement it represents is a tautology. In practice, you can ignore any tautologous clauses, since they don't do anything to the outcome of the resolution process.

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!

$\endgroup$
3
  • $\begingroup$ Thanks!! so seeing this from the other side, if i get an empty clause, then it means that the original sentence is a tautology? $\endgroup$ – Cipher Apr 16 '20 at 0:52
  • $\begingroup$ @Cipher Correct. The empty clause corresponds to a contradiction, so being able to resolve to an empty clause means that you are able to derive a contradiction from if the negation of the original statement, and that means that the original statement apparently cannot be false, and is therefore indeed a tautology. $\endgroup$ – Bram28 Apr 16 '20 at 11:33
  • $\begingroup$ @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$. $\endgroup$ – Bram28 Apr 16 '20 at 13:44

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.