Soluzione lab 03 02 2022

Page 1

begin_problem ( Problem ) . list_of_descriptions . name ({* appello -03 -02 -2022*}) . author ({**}) . status ( unsatisfiable ) . description ({**}) . date ({**}) . end_of_list . list_of_symbols . predicates [(R,2) ,(A,1), (B,1) ]. %R formalizza il collegamento tra 2 nodi %A formalizza essere di tipo A %B formalizza essere di tipo B % Si poteva anche utilizzare un solo predicato unario per indicare % il tipo (A ad esempio), e utilizzare la negazione di quel predicato % per indicare l'altro tipo. end_of_list . list_of_formulae(axioms). % Ogni nodo è di tipo A o di tipo B formula(forall([x],or(A(x),B(x)))). % Non ci sono autoanelli formula(forall([x],not(R(x,x)))). % Sono in relazione solo nodi di tipo diverso formula(forall([x,y],implies(R(x,y),or(and(A(x),B(y)),and(A(y),B(x)))))). % La relazione R è transitiva formula(forall([x,y,z],implies(and(R(x,y),R(y,z)),R(x,z)))). % Ogni nodo di tipo B è in relazione con almeno un altro nodo formula(forall([x],implies(B(x),exists([y],R(x,y))))). % Le seguenti formule non erano esplicite nel testo: % Un nodo non può essere sia di tipo A che di tipo B formula(forall([x],not(and(A(x),B(x))))). % La relazione R è simmetrica formula(forall([x,y],implies(R(x,y),R(y,x)))). end_of_list . list_of_formulae(conjectures). % Esiste almeno un nodo di tipo A che non è in comunicazione con nessun altro formula(exists([x],and(A(x),forall([y],not(R(x,y)))))). end_of_list . list_of_settings(SPASS). {* set_flag(DocProof,1). *} end_of_list. end_problem.