Let's assume I have the following 3 clauses:
$\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$

and I want to see if our KB entails $\neg U$ so I tried to apply the resolution algorithm like below:

$$ (\neg P \lor Q \lor S \lor T) \land \neg T \land \neg Q \land (\neg U \lor T \lor \neg S) \land (\neg U \lor T \lor P) \land U $$ By applying the algorithm on the first two clauses we'll have: $$ (\neg P \lor Q \lor S) \land (\neg Q) \land (\neg U \lor T \lor \neg S) \land (\neg U \lor T \lor P) \land U $$ Again by applying the algorithm on the first two clauses we'll have: $$ (\neg P \lor S) \land (\neg U \lor T \lor \neg S) \land (\neg U \lor T \lor P) \land U $$ By applying full resolution on the first two clauses(for $S$) we'll have: $$ (\neg P \lor \neg U \lor T) \land (\neg U \lor T \lor P) \land U\\ \rightarrow (\neg U \lor T) \land U\\ \rightarrow T $$ I don't know where to go from here. Obviously, our knowledge base entails $\neg U$ and the resolution algorithm is supposed to be complete, but I don't know which step in my solution is wrong.


1 Answer 1


Here is a simpler example. The clauses $A \lor B$, $\lnot A$, $A$ are clearly contradictory. Applying resolution, we resolve the first two clauses, and are left with the two clauses $B$ and $A$. Now we are stuck.

Your issue is similar. When applying the Resolution rule, we don't remove the resolved clauses. Rather, we retain them. The completeness of Resolution states that if the original clauses are unsatisfiable, then there is a way to repeatedly apply the Resolution rule, not removing the resolvents, that will eventually produce the empty clause. In fact, the following rule will work:

Repeat until no longer possible: resolve a pair of clauses which produce a clause not already present.

  • $\begingroup$ I still don't get it. Are we supposed to do it in an order? $\endgroup$
    – user127875
    Dec 17, 2021 at 12:44
  • $\begingroup$ Spend more time thinking about it. $\endgroup$ Dec 17, 2021 at 12:44
  • $\begingroup$ By the way, in Resolution we don't replace resolved clauses with their resolvent. Rather, we add the resolved clause to the list of known clauses. $\endgroup$ Dec 17, 2021 at 12:46
  • $\begingroup$ Oh, so I can still resolve T with its negated literal to get an empty clause. Correct me if I'm wrong but even in your example, it is enough to create the empty clause by applying resolution on A and its negation. $\endgroup$
    – user127875
    Dec 17, 2021 at 13:21
  • $\begingroup$ Right, you can resolve $T$ with $\lnot T$ to find the empty clause. $\endgroup$ Dec 17, 2021 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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