# Resolution algorithm does not seem to generate the empty clause

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.

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.
• Right, you can resolve $T$ with $\lnot T$ to find the empty clause. Dec 17, 2021 at 15:14