Esame 3 febbraio sol

Pagina 1

Durata della prova: 1h 30’ Esame di Logica e Algebra Politecnico di Milano – Ingegneria Informatica – 03 F ebbraio 2022 Docente: Cognome: Nome: Codice persona: T utte le risposte devono essere motivate. Gli esercizi vanno svolti su questi fogli, nello spazio sotto il testo e sul retro. I fogli di brutta non devono essere consegnati. I compiti privi di indicazione leggibile di nome e cognome non verranno corretti. 1. (Punteggio:2.5+3.5, 3) (a) Verificare sia per via semantica sia usando la risoluzione che il seguente insieme di f.b.f.: Γ ={¬A,B∧C⇒ (A ⇐⇒ B),B⇒A,C∨ (B⇒¬C)} ` e soddisfacibile. (b) Verificare se Γ∪{¬ (¬A∧ (B⇒A)∧¬C)} ` e un insieme insoddisfacibile. Soluzione: (a) E’ immediato verificare che C∨ (B⇒¬C) ` e una tautologia, quindi i modelli di Γ e quelli di Γ′ ={¬A,B∧C⇒ (A ⇐⇒ B),B⇒A} coincidono. Dalle tavole di verit` a delle formule di Γ′ otteniamo i modelli di Γ ′ che sono solo due: ν1(A) =ν1(B) = ν1(C) = 0 e ν2(A) = ν1(B) = 0, ν2(C) = 1. Pertanto Γ ` e chiaramente un insieme soddisfacibile poich` e ammette almeno un modello. Con la risoluzione dobbiamo mostrare che dalle clausole di Γ ′ non ricaviamo quella vuota. Le clausole di Γ ′ sono le seguenti: • dalla prima formula si ricava{¬A}; • dalla seconda si ricava{¬B,A,¬C} (dato che la formula ` e semanticamente equivalente a¬B∨A∨¬C); • dalla terza formula si ricava{¬B,A}. Ora dalle tre clausole {¬A},{¬B,A,¬C},{¬B,A} vediamo subito che possiamo eliminare (pruning) le ultime due clausole che contengono ¬B (dato che non compare un B e quindi non potr` o mai “eliminarlo”) e quindi rimaniamo con la sola clausola {¬A} da cui non potr` o mai ottenre la clausola vuota, quindi Γ′ ` e soddisfacibile, e quindi anche Γ. Alternativamente bastava verificare che Ris(Γ′) = Γ ′∪{{¬B,¬C},{¬B}} =Ris2(Γ′) e, poich` e la clausola…