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.


1 Answer 1


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 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.