Computer Engineering - Logica e Algebra

Full exam

Logica e Algebra - 29 Gennaio 2019 - SPASS Cognome:Nome:Matricola: L'esercizio va svolto su questo foglio: nello spazio sotto il testo e sul retro la parte di SPASS. Eventuali fogli di brutta non devono essere consegnati e non verranno ritirati. I compiti privi di indicazione di nome e cognome NON verranno corretti. Si formalizzi il seguente problema in logica del primo ordine, speci cando il tipo sintattico di tutti i simboli extralogici che si ritiene di dover introdurre. In un insieme fattosolodi scatole e premi (i premi non sono scatole e quindi dobbiamo formalizzare anche questo fatto) si hanno le seguente regole: 1)Gli unici oggetti che possono contenere altri oggetti sono scatole; 2)La relazione di contenimento soddisfa la proprieta transitiva; 3)Nessuna scatola e vuota; 4)Se una scatolaxcontiene un premio, alloraxcontiene anche una scatola; Dalle precedenti regole dedurre che non esistono scatole che contengono solo premi. Si scriva un programma SPASS per veri care se il precedente fatto sussiste. Soluzione: Abbiamo bisogno di una lettera predicativa binariaC(x; y) per speci care che l'oggettoxcontiene l'oggettoy, e di due lettere predicative unarieS(x); P(x) per descrivere che un oggetto e rispettivamente una scatola o un premio. Dobbiamo speci care che scatole e premi partizionano l'insieme di tutti gli oggetti: possiamo farlo tramite la formula 8x(P(x), :S(x)) Mentre le regole possono essere formalizzate nel seguente modo:1.8x8y(C(x; y))S(x)) 2.8x8y8z((C(x; y)^C(y; z)))C(x; z)) 3.8x(S(x)) 9yC(x; y)) 4.8x(9y(S(x)^C(x; y)^P(y))) 9z(S(z)^C(x; z))) Dalle precedenti regole dobbiamo dedurre: :9x(S(x)^ 8y(C(x; y))P(y)) Formalizziamolo in SPASS: list_of_symbols.predicates[(C,2), (S,1), (P,1)]. end_of_list. list_of_formulae(axioms). formula(forall([x],equiv(P(x),not(S(x))))). formula(forall([x],forall([y],implies(C(x,y),S(x))))). formula(forall([x,y,z],implies(and(C(x,y),C(y,z)),C(x,z)))). formula(forall([x],implies(exists([y],and(S(x),C(x,y),P(y))),exists([z],and(S(z),C(x,z)))))). formula(forall([x],implies(S(x),exists([y],C(x,y))))). end_of_list. list_of_formulae(conjectures). formula(not(exists([x],and(S(x),forall([y],implies(C(x,y),P(y))))))). end_of_list.