Full exam for Logica e Algebra in the Computer Engineering degree programme at Politecnico di Milano. The document covers: 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
Full exam for Logica e Algebra in the Computer Engineering degree programme at Politecnico di Milano. The document covers: 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
Import quality: text was extracted directly from the original document.
Representative passages recognised in different parts of the material. The full extracted text remains available to search, while this compact preview makes the page easier to read.
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.
First page of the document.
