Full exam for Logica e Algebra in the Computer Engineering degree programme at Politecnico di Milano. The document covers: begin_problem(Skeleton). list_of_descriptions. name({**}). author({**}). status(unknown). description({*Skeleton of spass coding*}). end_of_list. list_of_symbols. functions[(f,1),(m,0)]. predicates[(R,2),(S,1)]. end_of_list. list_of_formulae(axioms). % assiomi di poset
Full exam for Logica e Algebra in the Computer Engineering degree programme at Politecnico di Milano. The document covers: begin_problem(Skeleton). list_of_descriptions. name({**}). author({**}). status(unknown). description({*Skeleton of spass coding*}). end_of_list. list_of_symbols. functions[(f,1),(m,0)]. predicates[(R,2),(S,1)]. end_of_list. list_of_formulae(axioms). % assiomi di poset
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(Skeleton). list_of_descriptions. name({**}). author({**}). status(unknown). description({*Skeleton of spass coding*}). end_of_list. list_of_symbols. functions[(f,1),(m,0)]. predicates[(R,2),(S,1)]. end_of_list. list_of_formulae(axioms). % assiomi di poset formula(forall([x],R(x,x))). formula(forall([x,y],implies(and(R(x,y),R(y,x)),equal(x,y)))). formula(forall([x,y,z],implies(and(R(x,y),R(y,z)),R(x,z)))). % f preserva l'ordine formula(forall([x,y],implies(R(x,y),R(f(x),f(y))))). % m è minimale formula(forall([x],implies(R(x,m),equal(m,x)))). % definizione di tipo di S formula(forall([x], equiv(S(x),equal(f(x),m)))). end_of_list. list_of_formulae(conjectures). formula(forall([x,y,z],implies(and(S(x),S(y),R(x,z),R(z,y)),S(z)))). % congettura senza aver definito il tipo S formula(forall([x,y,z],implies(and(equal(f(x),m),equal(f(y),m),R(x,z),R(z,y)),equal(f(z),m)))). end_of_list. list_of_settings(SPASS). {* set_flag(DocProof,1). *} end_of_list. end_problem.
First page of the document.
