Soluzioneprovadilaboratorio27luglio2016

Pagina 1

Logica e Algebra 27 luglio 2016 - SPASS “Gli studenti in corso e i laureandi hanno studiato a sufficienza 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 sufficienza. 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 verificare 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: • Cor(x) con il significato di “la persona x ` e uno studente in corso” • Lau(x) con il significato di “la persona x ` e un laureando ” • Suf (x) con il significato di “la persona x ha studiato a sufficienza per l’esame di Logica e Algebra” • Att(x) con il significato di “la persona x non ha seguito il corso con attenzione” • Lam(x) con il significato di “la persona x ha osato lamentarsi dell’esame di SPASS” Il problema si formalizza allora in logica del I ordine cos` ı: Assiomi • Gli studenti in corso e i laureandi hanno studiato a sufficienza per l’esame di Logica e Algebra o non hanno seguito il corso con attenzione: ∀x((Cor(x)∨ Lau(x))⇒ (Suf (x)∨ Att(x))) • Chiunque osi lamentarsi del compito di SPASS deve essere un laureando o non aver seguito il corso con attenzione: ∀x(Lam(x)⇒ (Lau(x)∨ Att(x))) • Di certo gli studenti in corso hanno studiato a sufficienza: ∀x(Cor(x)⇒ Suf (x)) • Qualcuno ha osato lamentarsi: ∃xLam(x) Congettura Qualche laureando non ha seguito il corso con attenzione: ∃x(Lau(x)∧ Att(x)) Un programma Spass per verificare la tesi…