I have a set of clauses in CNF. I have to prove that $not[notR,notP,notQ]$ is NOT a logical consequence of this set of clauses.
What i did is :
1)The goal clause becomes : $R\wedge P\wedge Q$.I dont need to negate that the goal clause since i want to prove that it is NOT a logical consequence. I can rewrite the goal clause as :
R.
P.
Q.
2) Now, i have to use the resolution principle to obtain an empty clause. If i get it, then $not[notR,notP,notQ]$ is NOT a logical consequence of the set of clauses.
Is it correct ?
OK, so suppose you add the clauses $\{ A \}$, $\{ B \}$, and $\{ C \}$, to your clause set, and you are able to derive an empty clause. Well, that means that your original clause set $\Gamma$, together with these three clauses leads to a contradiction. Well, that means that the original clause set $\Gamma$ logically implies the negation of $A \land B \land C$, i.e the original clause set implies $\neg A \lor \neg B \lor \neg C$.
OK, but that does not mean that its negation is not a logical consequence of that clause set. For example, if the original clause set contains a contradiction, then it will logically imply both $\neg A \lor \neg B \lor \neg C$ as well as $\neg (\neg A \lor \neg B \lor \neg C)$
So, what you need to do instead is to find an assignment that sets all of the clauses in $\Gamma$ to true, but that sets $\neg (\neg A \lor \neg B \lor \neg C)$ to false, i.e. $\neg A \lor \neg B \lor \neg C$ to true. Or, in other words, you need to show that the set of statements $\Gamma \cup \neg A \lor \neg B \lor \neg C$ is consistent.
Now, I am not sure resolution is the best method for this, since resolution is really a method to show inconsistency, rather than consistency. The only way to use resolution to show consistency of $\Gamma \cup \neg A \lor \neg B \lor \neg C$, is to start with $\Gamma \cup \neg A \lor \neg B \lor \neg C$ as your clauses, and to then demonstrate (in a meta-sort-of-way) that at some point it is impossible to generate any new clauses, while not having derived a contradiction. But, my advise is to use a different method. Do you have few enough variables to just do a simple truth-table?