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

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.