Provadilaboratorio13febbraio2020

Page 1

Logica e Algebra - 13 febbraio 2020 - SPASS Cognome: Nome: Matricola: L’esercizio va svolto su questo foglio: nello spazio sotto il testo e sul retro la parte di SP ASS. 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 i seguenti teoremi della teoria dei semigruppi in logica del primo ordine, specificando il tipo sintattico di tutti i simboli extralogici che si ritiene di dover introdurre. Si scriva poi un programma SPASS per verificarne la correttezza. Teorema. Sia (C,·) un semigruppo cancellativo (un semigruppo si dice cancellativo se in esso valgono le leggi di cancel- lazione, cio` e seab = ac allora b = c e se ba = ca allora b = c) senza elemento neutro e sia R la relazione su C definita da (a, b)∈R se e solo se aC∪{ a} = bC∪{ b} (dove aC ={ac| c∈ C}); alloraR ` e la relazione identit` a. Soluzione. Per formalizzare il problema basta una lettera funzionale binaria per rappresentare l’operazione del semigruppo, ed una predicativa binaria per rappresentare la relazione L. Gli assiomi e la congettura sono semplici ad eccezione della definizione diL che richiede di esprimere l’uguaglianza tra insiemi, cosa che va fatta imponendo la doppia inclusione tra i due. begin_problem(esame13022020). list_of_descriptions. name({*esame-del-13-02-2020*}). author({*J. Howie*}). status(unsatisfiable). description({*Fundamentals of Semigroup Theory*}). end_of_list. list_of_symbols. functions[(p,2)]. predicates[(R,2)]. end_of_list. list_of_formulae(axioms). %l’operazione ` e associativa formula(forall([x,y,z],equal(p(x,p(y,z)),p(p(x,y),z)))). %valgono le leggi di cancellazione formula(forall([x,y,z],implies(equal(p(x,y),p(x,z)),equal(y,z)))).…