How would one apply the resolution rule to $\{q;\neg q\}\{q;\neg q\}$? Would one obtain

  1. $\{q;\neg q\}$?

  2. $\{q;\neg q\}$?

  3. something else?

I thought it would result in the empty set, yet it seems that it ends with the same set $\{q;\neg q\}$. Why?

From Wikipedia

The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two clauses containing complementary literals. A literal is a propositional variable or the negation of a propositional variable. Two literals are said to be complements if one is the negation of the other (in the following, $\lnot c$ is taken to be the complement to $c$). The resulting clause contains all the literals that do not have complements.

A simple example

$$\frac{a \vee b, \quad \neg a \vee c}{b \vee c}$$

In plain language: Suppose $a$ is false. In order for the premise $a \vee b$ to be true, $b$ must be true. Alternatively, suppose $a$ is true. In order for the premise $\neg a \vee c$ to be true, $c$ must be true. Therefore regardless of falsehood or veracity of $a$, if both premises hold, then the conclusion $b \vee c$ is true.


If we apply the resolution rule first to 1 and 2 deleting the couple $q$ (of 1) and $\lnot q$ (of 2), we get 3 : $\{ q; ¬q \}$.

But $\{ q; ¬q \}$ is a clause, i.e. a disjunction of literals, and the formula $q \lor \lnot q$ is a tautology.

Thus, we cannot derive the empty clause, and we have to conclude that the initial set of clauses is satisfiable (which must be evident, being formed by tautologies).


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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