Esercizio: • Mostrare che: – P = A ⇒ C • è una conseguenza

Esercizio:
• Mostrare che:
– P =A⇒C
• è una conseguenza semantica di:
– S = {A ⇒ (B ⇒ C), A ⇒ B}
Soluzione:
Metodo di Risoluzione:
S P quindi dobbiamo mostrare che:
S C ∪ (∼ P )C è insoddisfacibile
Per prima cosa dobbiamo trovare S a clausole (cercando la FNC):
S = {A ⇒ (B ⇒ C), A ⇒ B}
= {∼ A ∨ (∼ B ∨ C), ∼ A ∨ B}
= {(∼ A∨ ∼ B ∨ C), (∼ A ∨ B)}
quindi S C = {{∼ A, ∼ B, C}, {∼ A, B}}
Ora troviamo ∼ P a clausole (cercando la FNC):
∼ P =∼ (A ⇒ C)
=∼ (∼ A ∨ C)
= A∧ ∼ C
quindi (∼ P )C = {{A}, {∼ C}}
S = S C ∪ (∼ P )C
R=S
Ris(S) = S ∪ {{∼ A, C}, {B}, {∼ B, C}, {∼ A, ∼ B}} = S 0
S’ non è vuoto ed è diversa da S, quindi dobbiamo andare avanti.
R = S’
Ris(S’) = S 0 ∪ {{∼ A}, {C}, {∼ B}} = S”
S” non è vuoto ed è diversa da S’, quindi dobbiamo andare avanti.
R = S”
Ris(S”) = S 00 ∪ {, . . .} insoddisfacibile, quindi S P
Metodo di Refutazione:
C1
C2
C3
C4
= {∼ A, B} clausola di S C
= {A} clausola di (∼ P )C
= {B} risolvente di C1 e C2
= {∼ A, ∼ B, C} clausola di S C
1
C5
C6
C7
C8
= {∼ B, C} risolvente di C4 e C2
= {∼ C}clausola di (∼ P )C
= {∼ B} risolvente di C5 e C6
= risolvente di C7 e C3
2