logo
  • userLoginStatus

Welcome

Our website is made possible by displaying online advertisements to our visitors.
Please disable your ad blocker to continue.

Current View

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 a ermazioni 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.