1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

See :

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.

$\endgroup$
  • $\begingroup$ So, for example if we get to the last literal, S, and our remaining clauses are {P} and {S}, then we will eliminate S. But, we will still have the {P}, so it is satisfiable. $\endgroup$ – name Feb 23 '17 at 11:11
  • $\begingroup$ @name - if we have only two clause : $\{ P \}$ and $\{ S \}$, they are clearly satisfiable. They are equiv to $P \land S$. $\endgroup$ – Mauro ALLEGRANZA Feb 23 '17 at 12:13

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.