Will this be a correct way in using the Davis Putnam Procedure in Propositional Logic?

Question

I can't really find much information about this topic, so it is difficult to know if I'm doing this right. Any feedback will be much appreciated. Thanks!

(¬P → Q) ∧ ((Q ∧ R) → S) ∧ ¬(¬(P → R)) ⊨ S

Convert to CNF:

(P v Q) ∧ (¬ (Q ∧ R) v S) ∧ (¬P v ¬R)

(P v Q) ∧ (¬Q v ¬R v S) ∧ (¬P v R)

Negation of Conclusion: ¬S

Convert F to clause form:
F = (P v Q) ∧ (¬Q v ¬R v S) ∧ (¬P v R) ∧ ¬S

≡ {{P, Q}, {¬Q, ¬R, S}, {¬P, R}, {¬S}}

Proof by David-Putnam procedure:

Set of Literals of F = {P, Q, R, S}

By P: New clauses using Resolution on P: {R}

      F = {{P, Q}, {¬Q, ¬R, S},  {¬P, R}, {¬S}, {R}}

      Discard all clauses with P or ¬P in them.

      F = {{¬Q, ¬R, S}, {¬S}, {R}}

By Q: New clauses using Resolution on Q: {¬R v S}

      F = {{P, Q}, {¬Q, ¬R, S},  {¬P, R}, {¬S}, {R}, {¬R v S}}

      Discard all clauses with Q or ¬Q in them.

      F = {{¬P, R}, {¬S}, {R}, {¬R v S}}

By R: New clauses using Resolution on R: {S}

      F = {{¬P, R}, {¬S}, {R}, {¬R v S}, {S}}

      Discard all clauses with R or ¬R in them.

      F = {{¬S}, {S}}

By S: New clauses using Resolution on S: { }

      F = {{¬S}, {S}, { }}

      Discard all clauses with S or ¬S in them.

      F = { }

Are output is the empty clause, so F is unsatisfiable, therefore the Claim is true

Answer 1

See :

• Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), Ch.6.2 Davis-Putnam Algorithm, page 115:

Input: A formula $F$ in clausal form.

Output: Report that $F$ is satisfiable or unsatisfiable.

Perform the following rules repeatedly, but the third rule is used only if the first two do not apply:

Unit-literal rule: If there is a unit clause $\{ l \}$, delete all clauses containing $l$ and delete all occurrences of $l^c$ from all other clauses.

Pure-literal rule: If there is a pure literal $l$ [i.e. a literal $l$ that appears in at least one clause of $S$, but its complement $l^c$ does not appear in any clause of $S$], delete all clauses containing $l$.

Eliminate a variable by resolution: Choose an atom $p$ and perform all possible resolutions on clauses that clash on $p$ and $\lnot p$. Add these resolvents to the set of clauses and then delete all clauses containing $p$ or $\lnot p$.

Terminate the algorithm under the following conditions:

If empty clause $\square$ (or: $\{ \}$) is produced, report that the formula is unsatisfiable.

If no more rules are applicable, report that the formula is satisfiable.

---

We have to apply it to the set $F_0$ of clauses:

$F_0 = \{ \{ P, Q \}, \{ ¬Q, ¬R, S \}, \{ ¬P, R \}, \{¬S \} \}$.

1) Apply Unit-literal rule : delete $\{¬S \}$ and delete all occurences of $S$.

Result: $F_1 = \{ \{ P, Q \}, \{ ¬Q, ¬R, \}, \{ ¬P, R \} \}$.

2) Apply Resolution with $P$. Result: $F_2 = \{ \{ Q, R \}, \{ ¬Q, ¬R, \} \}$.

3) Apply Resolution with $Q$. Result: $F_3 = \{ \{ R, ¬R \} \}$.

No more rules are applicable, and thus the formula $F$ is satisfiable, i.e.:

$(¬P → Q) ∧ ((Q ∧ R) → S) ∧ ¬(¬(P → R)) \nvDash S$.

Check: with a valuation $v$ such that $v(S)=v(Q)=$ f and $v(P)=v(R)=$ t, the premise is t and the conlcusion is f.