Laboratory 07072016

Pagina 1

Logica e algebra 7 luglio 2016 Laboratorio Chiamiamo preordine su un insieme X una relazione binaria R su X che sia riflessiva e transitiva. Per ogni x,y ∈ X, definiamo sup(x,y) rispetto ad R in modo analogo a quanto fatto per una relazione d’ordine (ovvero sup(x,y ) è un elemento z ∈X tale che (x,z) ∈R, (y,z) ∈R e, per ogni v ∈X, se (x,v) ∈R e (y,v) ∈R allora (z,v) ∈R). Diciamo che una funzione f:X →X preserva Il preordine R se per ogni x,y ∈X, (x,y) ∈R implica (f(x),f(y)) ∈R, e diciamo che f preserva il sup se supposto z=sup(x,y) si ha f(z)=sup(f(x),f(y)). Scelto un opportuno linguaggio del I ordine, formalizzare il seguente enunciato. Sia R un preordine su X, siano f e g funzioni da X ad X che preservano R tali che (f(x),y) ∈R se e solo se (x,g(y)) ∈R. Allora f preserva anche il sup. Scrivere poi un programma SPASS per verificare l’enunciato. Soluzione Il nostro linguaggio deve contenere una lettera predicativa R di arità 2 e due lettere funzionali f, g di arità 1. E’ utile far uso delle seguenti abbreviazioni per formalizzare il problema: U(x,y,z) ≡R(x,z) ∧R(y,z) per indicare che z è un “maggiorante” di x ed y rispetto ad R S(x,y,z) ≡(U(x,y,z) ∧∀w(U(x,y,w) ⇒R(z,w) per indicare che z=sup(x,y) Utilizzando anche questa estensione del linguaggio l’enunciato può essere espresso dalle seguenti formule: R è un preordine : ∀xR(x,x) ; ∀x∀y∀z(R(x,y) ∧R(y,z) ⇒R(x,z) f e g preservano il preordine : ∀x∀y(R(x,y) ⇒R(f(x),f(y)), ∀x∀y(R(x,y) ⇒R(g(x),g(y)) legame fra f e g: ∀x∀y(R(f(x),y) ⇔R(x,g(y)) f preserva il sup: ∀x∀y∀z(S(x,y,z) ⇒S(f(x),f(y),f(z)) Il codice SPASS, rimuovendo le abbreviazione, è. begin_problem(POA). list_of_descriptions. name({**}). author({**}). status(unknown). description({**}). end_of_list. list_of_symbols. functions[(f,1),(g,1)]. predicates[(R,2)].…