Soluzioneprovalaboratorio10febbraio2021

Pagina 1

Durata della prova: 30’ Esame di Logica e Algebra Politecnico di Milano – Ingegneria Informatica – 10 febbraio 2021 – SP ASS Scrivere un programma SPASS per verificare la correttezza del seguente ragionamento. Specificare nei commenti il tipo sintattico di tutti i simboli extralogici che si ritiene di dover introdurre. In un insieme di nazioni, una nazione pu` o dichiarare guerra ad un’altra o allearsi, ma non entrambe le cose. Se un certo paese X si allea (o fa la guerra) al paese Y allora vale anche il viceversa. Inoltre un paese non fa mai la guerra a se stesso. Vale la regola che il nemico del mio nemico ` e mio amico con cui ovviamente mi alleo. Mostrare che se ci sono almeno tre nazioni distinte, due si alleano. Soluzione. L’idea ` e quella di considerare come dominio l’insieme delle nazioni, avremo poi bisogno di due predicati binari, diciamo G, A, per indicare che una certa nazione fa guerra ad un’altra oppure si allea con essa. Allora le varie affermazioni si tradurranno cos` ı: • una nazione pu` o dichiarare guerra ad un’altra o allearsi, ma non entrambe le cose: ∀x∀y¬(G(x, y) ∧ A(x, y)) • se un certo paese X si allea (o fa la guerra) al paese Y allora vale anche il viceversa: ∀x∀y((A(x, y) ⇒ A(y, x)) ∧ (G(x, y) ⇒ G(y, x))) • un paese non fa mai la guerra a se stesso: ∀x¬G(x, x) • il nemico del mio nemico ` e mio amico con cui ovviamente mi alleo: ∀x∀y∀z((G(x, y) ∧ G(y, z)) ⇒ A(x, z)) • se ci sono almeno tre nazioni distinte, due si alleano: ∃x∃y∃z(¬(x = y) ∧ ¬(x = z) ∧ ¬(y = z)) ⇒ ∃x∃yA(x, y) Un programma SPASS per verificare se quest’ultima formula ` e conseguenza delle prime quattro ` e il seguente: b e g i n _ p r o b l e m ( Problem ) . l i s t _ o f _ d e s c r i p t i o n s . name ({* esame -10 -02 -2021*}) . author ({**}) . status ( u n s a t i s f i a b…