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 ) ) ) ) .