Direct proof (Logic)

Question

I need help, I've to give by resolution a direct proof of

I've made a conjunction and got:

How do I give a direct proof by resolution?

Answer 1

Starting from Mauro's answer we have 1. ¬P∨Q, 2. ¬S∨Q, and 3. P∨Q$\lor$¬R. Applying resolution to 1. and 3. we obtain

Q$\lor$$\lnot$R, which is your conclusion. If you need to get to the empty clause, then you can assume R and $\lnot$Q, since $\lnot$($\lnot$R$\lor$Q) is logically equivalent to R$\land$$\lnot$Q.

Answer 2

In order to apply Resolution to :

$\alpha, \beta \vDash \delta$ ---(*)

you have to consider the formula :

$\alpha \land \beta \land \lnot \delta$ ---(§)

i.e. to consider the conjunction of all the premises and the negation of the sentence to be proved.

This is so because (*) holds iff $\alpha \land \beta \rightarrow \delta$ valid, and this holds iff its negation, which is (§), is contradictory, or identically false.

But (§) is contradictory iff the set of formulae $\Sigma = \{ \alpha, \beta, \lnot \delta \}$ is unsatisfiable.

Thus, the sentence (§) is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set $\Sigma$ of clauses, where a clause is a finite disjunction of literals.

---

Thus, if we apply the procedure to our example, we have :

(i)

$(\lnot P \land \lnot S) \lor Q$

which, by distributivity is :

$(\lnot P \lor Q) \land (\lnot S \lor Q)$.

Then we have :

(ii)

$P \lor Q \lor \lnot R$

which is already a clause.

Finally the negation of the conclusion :

(iii)

$\lnot (\lnot R \lor Q)$

which is :

$R \land \lnot Q$.

Now we form the conjunction of all the clauses :

$(\lnot P \lor Q) \land (\lnot S \lor Q) \land (P \lor Q \lor \lnot R) \land R \land \lnot Q$.

From it, we get the set

$\Sigma = \{ \lnot P \lor Q, \lnot S \lor Q, P \lor Q \lor \lnot R, R, \lnot Q \}$.

Now we apply the resolution rule

it is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set $\Sigma$, it is added to $\Sigma$, and is considered for further resolution inferences.

(i) Consider : $P \lor Q \lor \lnot R$ and $R$ and simplify to $P \lor Q$ which must be added to $\Sigma$.

(ii) Consider $P \lor Q$ and $\lnot P \lor Q$ and simplify to $Q$, adding it to $\Sigma$.

(iii) Consider $Q$ and $\lnot Q$ and simplify to the empty clause : $\square$.

The empty clause is unsatisfiable; thus also $\Sigma$ is.

Having showed that

$\alpha \land \beta \land \lnot \delta$

is unsatisfiable, we can conlude with :

$\alpha, \beta \vDash \delta$.

---

Comment

The first key point of the method is the simplification of $A \lor P$ and $B \lor \lnot P$ into $A \lor B$.

This amounts simply to $A \lor P, B \lor \lnot P \vDash A \lor B$, which is nothing more than an application of syllogism : $\lnot A \rightarrow P, P \rightarrow B \vDash \lnot A \rightarrow B$.

Thus, the simplification steps amount to starting from the formula $\alpha \land \beta \rightarrow \lnot \delta$, rewrite it as a set of clauses $\Sigma$ and then simplify $\Sigma$ though resolution rule.

The other key point of the method is the simplification of $Q$ and $\lnot Q$ to produce the empty clause : $\square$.

Forget about the "square" and rewrite $\Sigma$ as the conjunction of the clauses in it.

We get :

$[Q \land (\lnot S \lor Q) \land \lnot Q] \equiv [(Q \land \lnot Q) \land (\lnot S \lor Q)]$.

But $Q \land \lnot Q$ is a contradiction, i.e. is always false; thus the last formula is simply :

$False \land (\lnot S \lor Q)$

and $False \land A \equiv False$, for $A$ whatever, and this is enough to conclude that $\Sigma$ is unsatisfiable (to prove the conclusion with the above method, we have to produce the empty clause and not to transform $\Sigma$ into the empty set ...).