Resolution (Propositional Logic)

Resolution is an alternate method of evaluating propositions (instead of truth tables). It is a more complex process, but is much more useful for complex propositions, where the number of atoms is too large for a truth table.

A truth table is a good choice for propositions involving 3 or less atoms, since, at most, we need $2^3$ rows. However, even with just 5 atoms, we would need to make $2^5=32$ rows, which is very tedious. Resolution methods provide an alternate way to evaluate propositions.

Resolution Rule §

The resolution rule involves observing the implications involving contradicting atoms (e.g. $P$ and $\neg P$) to simplify a logical proposition.

Take the simplest of such forms:

$$(P\to Q)\wedge (\neg P\to R)$$

We can use the contrapositive of ($P\to Q$)

$$\equiv (\neg Q\to \neg P)\wedge (\neg P\to R)$$

then convert the implication ($\to$) to its logically equivalent disjunction-negation form:

$$\equiv (Q\vee \neg P)\wedge (\neg P\vee R)$$

and then use distributivity:

$$\equiv (Q\wedge \neg P)\vee (Q\wedge R)\vee (\neg P\wedge \neg P)\vee (\neg P\wedge R)$$

Finally, we simplify:

#tosee now what??

In summary, the resolution rule boils down to:

$$\begin{array}{rl}\cancel{P}& \to Q\\ \cancel{\neg P}& \to R\\ \therefore Q& \vee R\end{array}$$

or in terms of disjunctions:

$$\begin{array}{rl}\cancel{P}& \vee R\\ \cancel{\neg P}& \vee Q\\ \therefore Q& \vee R\end{array}$$

Resolution Tree §

A more straightforward, visual, way is to write all the statements we know to be true (our premises) row-wise or column-wise, and create a resolution binary tree, where our leaf nodes are our premises and any other node is a conclusion.

For example, take the following premises:

$$A\vee \neg BB\vee C\neg C$$

%%🖋 Edit in Excalidraw, and the dark exported image%%

If we add a fourth condition, $\neg A$, then we conclude a contradiction (which is a refutation, see below)

%%🖋 Edit in Excalidraw, and the dark exported image%%

Do not 'cancel out' more than one variable per step

While the we can conclude $P$ from the premise $(P\vee Q)\wedge \neg Q$ (by cancelling out $P$) in a single step, we cannot do the same for multiple variables in one step:

1. Take the premise $(P\vee Q)\wedge (\neg P\vee \neg Q)$
2. We cannot conclude $\perp$ from this by trying to cancel out $P$ and $Q$.
3. The premises are actually satisfiable, for example with P being true and Q being false

Formal Resolution Proofs §

Examples §

Non-examples §