Computer Engineering - Logica e Algebra

Full exam

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(f orall([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 s enza 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.