Computer Engineering - Logica e Algebra

Full exam

Logica e Algebra 27 luglio 2016 - SPASS \Gli studenti in corso e i laureandi hanno studiato a sucienza per l'esame di Logica e Algebra o non hanno seguito il corso con attenzione. Chiunque osi lamentarsi del compito di SPASS deve essere un laureando o non aver seguito il corso con attenzione. Di certo gli studenti in corso hanno studiato a sucienza. Qualcuno ha osato lamentarsi. Dunque qualche laureando non ha seguito il corso con attenzione." Formalizzare il ragionamento in logica del I ordine e scrivere un programma SPASS per vericare la tesi. Il ragionamento e corretto? Soluzione Considerando come dominio dell'interpretazione l'insieme degli studenti, abbiamo sicuramente bisogno di introdurre cinque lettere predicative unarie: C or(x) con il signicato di \la personaxe uno studente in corso" Lau(x) con il signicato di \la personaxe un laureando " S uf(x) con il signicato di \la personaxha studiato a sucienza per l'esame di Logica e Algebra" Att(x) con il signicato di \la personaxnon ha seguito il corso con attenzione" Lam(x) con il signicato di \la personaxha osato lamentarsi dell'esame di SPASS" Il problema si formalizza allora in logica del I ordine cos: AssiomiGli studenti in corso e i laureandi hanno studiato a sucienza per l'esame di Logica e Algebra o non hanno seguito il corso con attenzione:8x((C or(x)_Lau(x)))(S uf(x)_Att(x))) Chiunque osi lamentarsi del compito di SPASS deve essere un laureando o non aver seguito il corso con attenzione: 8x(Lam(x))(Lau(x)_Att(x))) Di certo gli studenti in corso hanno studiato a sucienza: 8x(C or(x))S uf(x)) Qualcuno ha osato lamentarsi: 9xLam(x) CongetturaQualche laureando non ha seguito il corso con attenzione: 9x(Lau(x)^Att(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 [ ( Cor , 1 ) , ( Lau , 1 ) , ( S u f , 1 ) , ( A t t , 1 ) , ( Lam , 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 ( o r ( Cor ( x ) , Lau ( x ) ) , o r ( S u f ( x ) , A t t ( x ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x ] , i m p l i e s ( L ( x ) , o r ( Lau ( x ) , A t t ( x ) ) ) ) ) . f o r m u l a ( f o r a l l ( [ x ] , i m p l i e s ( Cor ( x ) , S u f ( x ) ) ) ) . f o r m u l a ( e x i s t s ( [ x ] , Lam ( 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 ( e x i s t s ( [ x ] , and ( Lau ( x ) , A t t ( 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. Per provarlo basta descrivere un modello degli assiomi che non sia modello della congettura: in un modello contenete un unico individuoatale cheC or(a), S uf(a),Att(a) eLam(a) ma nonLau(a), le ipotesi sono soddisfatte ma non la tesi.