Soluzioneprova10febbraio2021

Pagina 1

Durata della prova: 1h 30’ Esame di Logica e Algebra Politecnico di Milano – Ingegneria Informatica – 10 F ebbraio 2021 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. (a) La formula ( A⇒B)⇒ (C⇒A) ` e un teorema della teoriaL? (b) Mostrare usando il metodo della risoluzione del primo ordine che la formula: F =∀x∀y ( (A(x,y )⇒∃y¬B(y))⇒ (∀zB(z)⇒¬A(x,y )) ) ` e logicamente valida. Soluzioni: Punteggio 9: a) 4; b) 5 (a) Dal teorema di correttezza e completezza della teoria L abbiamo che la assegnata formula ` e un teorema diL se e solo se risulta che ⊨ (A⇒B)⇒ (C⇒A), cio` e se e solo se la formula assegnata ` e una tautologia. Ora, invece di scrivere la tavola di verit` a, ragioniamo per assurdo e cerchiamo (se esiste) un eventuale assegnamento che renda falsa la formula. Questo assegnamentoν dovrebbe rendere vero l’antecedenteA⇒B e falso il conseguenteC⇒A, quindi ν(C) = 1 e ν(A) = 0 da cui si ottiene ν(A⇒ B) = 1. Quindi, per esempio, l’assegnamento ν(C) = 1, ν(A) = 0 e ν(B) = 1 rende la formula (A⇒B)⇒ (C⇒A) falsa e pertanto tale formula non ` e una tautologia e quindi non ` e un teorema diL. (b) Dobbiamo verificare se la formula ¬F ` e insoddisfacibile e quindi, per il teorema di correttezza e completezza per refutazione della risoluzione, se (¬F)c⊢R □. Portiamo in fnp la formula dell’esercizio: ∀x∀y ( (A(x,y )⇒∃y¬B(y))⇒ (∀zB(z)⇒¬A(x,y )) )≡ ∀x∀y (∃t(A(x,y )⇒¬B(t))⇒∃z(B(z)⇒¬A(x,y )) )≡ ∀x∀y∀t∃z ( (A(x,y )⇒¬B(t))⇒ (B(z)⇒¬A(x,y )) )≡ Neghiamo la formula ¬F≡∃ x∃y∃t∀z¬ ( (A(x,y )⇒¬B(t))⇒ (B(z)⇒¬A(x,y )) ) e portiamo in forma di Skolem:…