Computer Engineering - Logica e Algebra

Full exam

Logica e Algebra 10 luglio 2015Spass \Se uno stato della Comunita Europea incrementa eccessivamente il suo ex- port, allora tutti gli altri stati comunitari subiranno un declino economico. Gli stati europei in declino economico aumentano il loro decit oppure le tasse, ma l'aumento del decit provoca il declino economico di tutti gli stati comunitari, e d'altra parte l'aumento delle tasse aumenta a sua volta il decit. Dunque uno stato europeo, per non subire un declino economico, non dovrebbe incrementare eccessivamente il suo export." Formalizzare il ragionamento in logica del I ordine e scrivere un programma SPASS per vericare la tesi, individuando anche eventuali ipotesi sottintese. Soluzione Considerando come dominio dell'interpretazione l'insieme degli stati europei, abbiamo sicuramente bisogno di introdurre quattro lette predicative unarie: AE(x) con il signicato di \lo statoxaumenta eccessivamente il suo ex- port" DE(x) con il signicato di \lo statoxe in declino" AT(x) con il signicato di \lo statoxaumenta le tasse" AD(x) con il signicato di \lo statoxaumenta il suo decit" Inoltre, per formalizzare correttamente la frase \... tutti gli altri stati ..." e necessario usare il predicato binario di uguaglianza, che possiamo indicare con l'usuale simbolo \=" e che e nativamente presente in Spass. Il problema si formalizza allora in logica del I ordine cos: AssiomiSe uno stato della Comunita Europea incrementa eccessivamente il suo export, allora tutti gli altri stati comunitari subiranno un de- clino economico: 8x(AE(x)) 8(y)(:(x=y))DE(y))) Gli stati europei in declino economico aumentano il loro decit oppure le tasse:8x(DE(x))(AD(x)_AT(x)))  (ma) l'aumento del decit provoca il declino economico di tutti gli stati comunitari: 8(x)(AD(x)) 8(y)(DE(y))) (e) d'altra parte l'aumento delle tasse aumenta a sua volta il decit: 8(x)(AT(x))AD(x)) CongetturaDunque uno stato europeo, per non subire un declino economico, non dovrebbe incrementare eccessivamente il suo export: 8(x)(:(DE(x))) :(AE(x))) Un programma Spass per vericare la tesi e b e g i np r o b l e m ( P r o b l e m ) . l i s to fd e s c r i p t i o n s . name (f E s e r c i z i o g) . a u t h o r (f NULL g) . 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   g) . d a t e (f NULL g) . e n do fl i s t . l i s to fs y m b o l s . p r e d i c a t e s [ ( AE , 1 ) , ( DE, 1 ) , ( AT, 1 ) , ( AD , 1 ) ] . e n do fl i s t . l i s to ff 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 ] , i m p l i e s (AE( x ) ,f o r a l l ( [ y ] , i m p l i e s ( n o t ( e q u a l ( x , y ) ) , DE( y ) ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x ] , i m p l i e s (DE( x ) , o r (AT( x ) ,AD( x ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x ] , i m p l i e s (AD( x ) , f o r a l l ( [ y ] , DE( y ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x ] , i m p l i e s (AT( x ) ,AD( x ) ) ) ) . e n do fl i s t . l i s to ff 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 ( f o r a l l ( [ x ] , i m p l i e s ( n o t (DE( x ) ) , n o t (AE( x ) ) ) ) ) . e n do fl i s t . e n dp r o b l e m . che produce \completion found", ovvero la congettura non e conseguenza degli assiomi. Infatti in un modello contenete un unico stato la tesi non segue dalle ipotesi, anche succeda e necessario aggiungere agli assiomi il fatto che esistono almeno due stati , ovvero la formula 9x9y(:(x=y)) in Spass f o r m u l a ( e x i s t s ( [ x , y ] , n o t ( e q u a l ( x , y ) ) ) ) .