Computer Engineering - Logica e Algebra

Full exam

Durata della prova: 30' Esame di Logica e Algebra Politecnico di Milano { Ingegneria Informatica { 10 febbraio 2021 { SPASS Scrivere un programma SPASS per vericare la correttezza del seguente ragionamento. Specicare nei commenti il tipo sintattico di tutti i simboli extralogici che si ritiene di dover introdurre. In un insieme di nazioni, una nazione puo 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, diciamoG,A, per indicare che una certa nazione fa guerra ad un'altra oppure si allea con essa. Allora le varie aermazioni si tradurranno cos: ˆuna nazione puo dichiarare guerra ad un'altra o allearsi, ma non entrambe le cose: 8x8y:(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: 8x8y((A(x; y))A(y; x))^(G(x; y))G(y; x))) ˆun paese non fa mai la guerra a se stesso: 8x:G(x; x) ˆil nemico del mio nemico e mio amico con cui ovviamente mi alleo: 8x8y8z((G(x; y)^G(y; z)))A(x; z)) ˆse ci sono almeno tre nazioni distinte, due si alleano: 9x9y9z(:(x=y)^ :(x=z)^ :(y=z))) 9x9yA(x; y) Un programma SPASS per vericare se quest'ultima formula e conseguenza delle prime quattro e il seguente: b e g i n _ p r o b l e m ( P r o b l e m ) . l i s t _ o f _ d e s c r i p t i o n s . n a m e ( { * e s a m e - 1 0 - 0 2 - 2 0 2 1 * } ) .a u t h o r ( { * * } ) . s t a t u s ( u n s a t i s f i a b l e ) .d e s c r i p t i o n ( { * * } ) . d a t e ( { * * } ) . e n d _ o f _ l i s t . l i s t _ o f _ s y m b o l s . p r e d i c a t e s [ ( G , 2 ) , ( A , 2 ) ] . e n d _ o f _ l i s t . l i s t _ o f _ f o r m u l a e ( a x i o m s ) . f o r m u l a ( f o r a l l ( [ x , y ] , n o t ( a n d ( G ( x , y ) , A ( x , y ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x , y ] , a n d ( i m p l i e s ( A ( x , y ) , A ( y , x ) ) ,i m p l i e s ( G ( x , y ) , G ( y , x ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x , y ] , n o t ( G ( x , x ) ) ) ) . f o r m u l a ( f o r a l l ( [ x , y , z ] , i m p l i e s ( a n d ( G ( x , y ) , G ( y , z ) ) , A ( x , z ) ) ) ) . e n d _ o f _ l i s t .l i s t _ o f _ f o r m u l a e ( c o n j e c t u r e s ) . f o r m u l a ( i m p l i e s ( e x i s t s ( [ x , y , z ] , a n d ( n o t ( e q u a l ( x , y ) ) , n o t ( e q u a l ( x , z ) ) ,n o t ( e q u a l ( y , z ) ) ) ) , e x i s t s ( [ x , y ] , A ( x , y ) ) ) ) . e n d _ o f _ l i s t . e n d _ p r o b l e m . Il risultato ecompletion found, dunque la tesi non segue dalle tre ipotesi. Si ottiene invece la tesi se alle ipotesi si aggiunge la formula8x8y(G(x; y)_A(x; y)), non esplicitamente inferibile dal testo.