Soluzionedellaprovadel13febbraio2020

Page 1

Durata della prova: 1h 30’ Esame di Logica e Algebra Politecnico di Milano – Ingegneria Informatica – 13 F ebbraio 2020 V oto Lab. precedente & docente: Cognome: Nome: Matricola: 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. Si vuole vedere se la diagnostica di un server sia avviata o meno sapendo che sussistono le seguenti regole: (a) La diagnostica ` e avviata se accade che non riceva un segnale e sia occupato, oppure nel caso in cui non sia occupato. (b) Se la diagnostica non ` e avviata allora vuol dire che il segnale non ` e arrivato e che il server non ` e occupato. Dopo aver formalizzato il problema nella logica proposizionale, mostrare sia per via semantica che con la risoluzione che la diagnostica ` e sempre avviata. Soluzioni: (a) Indichiamo con S la lettera enunciativa che indica che il segnale ` e stato ricevuto, O che il server ` e occupato, eD che la diagnostica ` e stata avviata. Allora la prima frase si traduce in (( ¬S∧ O)∨¬ O)⇒ D che ` e equivalente a (¬S∨¬ O)⇒ D. Mentre la seconda formula ` e ¬D⇒ (¬S∧¬ O). Dobbiamo mostrare sia per via semantica che con la risoluzione che {(¬S∨¬ O)⇒ D,¬D⇒ (¬S∧¬ O)} ⊨ D. Mediante la tabella di verit` a ` e semplice calcolare i modelli di {(¬S∨¬ O)⇒ D,¬D⇒ (¬S∧¬ O)} e si verifica che tutti questi modelli vi soddisfano vi(D) = 1, e quindi l’implicazione semantica vale. Mediante la risoluzione dobbiamo mostrare che l’insieme {(¬S∨¬ O)⇒ D,¬D⇒ (¬S∧¬ O),¬D} ` e insoddisfacibile. Per il teorema di correttezza e completezza per refutazione questo equivale a mostrare {(¬S∨¬ O)⇒ D,¬D⇒ (¬S∧¬ O),¬D}c⊢ □. Le clausole sono…