Computer Engineering - Logica e Algebra

Full exam

Logica e Algebra - 13 febbraio 2020 - SPASS Cognome:Nome:Matricola: L'esercizio va svolto su questo foglio: nello spazio sotto il testo e sul retro la parte di SPASS. Eventuali fogli di brutta non devono essere consegnati e non verranno ritirati. I compiti privi di indicazione di nome e cognome NON verranno corretti. Si formalizzi i seguenti teoremi della teoria dei semigruppi in logica del primo ordine, specicando il tipo sintattico di tutti i simboli extralogici che si ritiene di dover introdurre. Si scriva poi un programma SPASS per vericarne la correttezza. Teorema.Sia(C;
)un semigruppo cancel lativo (un semigruppo si dice cancel lativo se in esso valgono le leggi di cancel- lazione, cioe seab=acal lorab=ce seba=caal lorab=c) senza elemento neutro e siaRla relazione suCdenita da (a; b)2 Rse e solo seaC[ fag=bC[ fbg(doveaC=facjc2Cg); al loraRe la relazione identita. Soluzione. Per formalizzare il problema basta una lettera funzionale binaria per rappresentare l'operazione del semigruppo, ed una predicativa binaria per rappresentare la relazioneL. Gli assiomi e la congettura sono semplici ad eccezione della denizione diLche richiede di esprimere l'uguaglianza tra insiemi, cosa che va fatta imponendo la doppia inclusione tra i due. b e g i n _ p r o b l e m ( e s a m e 1 3 0 2 2 0 2 0 ) . 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 - d e l - 1 3 - 0 2 - 2 0 2 0 * } ) .a u t h o r ( { * J . H o w i e * } ) . 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 ( { * F u n d a m e n t a l s o f S e m i g r o u p T h e o r y * } ) . e n d _ o f _ l i s t . l i s t _ o f _ s y m b o l s .f u n c t i o n s [ ( p , 2 ) ] .p r e d i c a t e s [ ( R , 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 ) . % l ' o p e r a z i o n e e a s s o c i a t i v a f o r m u l a ( f o r a l l ( [ x , y , z ] , e q u a l ( p ( x , p ( y , z ) ) , p ( p ( x , y ) , z ) ) ) ) . % v a l g o n o l e l e g g i d i c a n c e l l a z i o n ef o r m u l a ( f o r a l l ( [ x , y , z ] , i m p l i e s ( e q u a l ( p ( x , y ) , p ( x , z ) ) , e q u a l ( y , z ) ) ) ) . f o r m u l a ( f o r a l l ( [ x , y , z ] , i m p l i e s ( e q u a l ( p ( y , x ) , p ( z , x ) ) , e q u a l ( y , z ) ) ) ) . % n o n c ' e u n e l e m e n t o n e u t r of o r m u l a ( n o t ( e x i s t s ( [ x ] , f o r a l l ( [ y ] , a n d ( e q u a l ( p ( x , y ) , y ) , e q u a l ( p ( y , x ) , y ) ) ) ) ) ) . % d e f i n i z i o n e d i Rf o r m u l a ( f o r a l l ( [ x , y ] , e q u i v ( R ( x , y ) ,a n d ( f o r a l l ( [ z ] , i m p l i e s( o r ( e q u a l ( z , x ) , e x i s t s ( [ t ] , e q u a l ( z , p ( x , t ) ) ) ) , o r ( e q u a l ( z , y ) , e x i s t s ( [ s ] , e q u a l ( z , p ( y , s ) ) ) ) ) ) , f o r a l l ( [ z ] , i m p l i e s( o r ( e q u a l ( z , y ) , e x i s t s ( [ t ] , e q u a l ( z , p ( y , t ) ) ) ) ,o r ( e q u a l ( z , x ) , e x i s t s ( [ s ] , e q u a l ( z , p ( x , s ) ) ) ) ) ) ) ) ) ) . 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 ) . % R e l ' i d e n t i t af o r m u l a ( f o r a l l ( [ x , y ] , e q u i v ( R ( x , y ) , e q u a l ( x , y ) ) ) ) .e n d _ o f _ l i s t . e n d _ p r o b l e m .