% luka - specification of a sequent calculus for 3-valued Lukasiewicz logic % Version 0.4 %option(tex_rulenames(on)). %option(tex_sequents(multidimensional)). %option(strategy(rule_ordering([nf,np,nt,af,ot,it,if,ip,at,of,ap,op]))). truth_values([f,p,t]). tex_tv(f,["f"]). tex_tv(p,["p"]). tex_tv(t,["t"]). % Implication % op(800, xfx, =>). tex_op((A=>B), ["(", A, bslash, "supset ", B, ")"]). rule((A=>B)^f, [[A^t],[B^f]], if). rule((A=>B)^p, [[A^p,B^p],[A^t,B^f]], ip). rule((A=>B)^t, [[A^f,A^p,B^t],[A^f,B^p,B^t]], it). tex_rn(if, ["{", bslash, "supset}", bslash, "colon f"]). tex_rn(ip, ["{", bslash, "supset}", bslash, "colon p"]). tex_rn(it, ["{", bslash, "supset}", bslash, "colon t"]). % Conjunction % op(600, yfx, &). tex_op((A&B), ["(", A, bslash, "land ", B, ")"]). rule((A&B)^f, [[A^f,B^f]], af). rule((A&B)^p, [[A^p,B^p],[A^p,A^t],[B^p,B^t]], ap). rule((A&B)^t, [[A^t],[B^t]], at). tex_rn(af, ["{", bslash, "land}", bslash, "colon f"]). tex_rn(ap, ["{", bslash, "land}", bslash, "colon p"]). tex_rn(at, ["{", bslash, "land}", bslash, "colon t"]). % Disjunction % op(700, yfx, v). tex_op((A v B), ["(", A, bslash, "lor ", B, ")"]). rule((A v B)^f, [[A^f],[B^f]], of). rule((A v B)^p, [[A^p,B^p],[A^p,A^f],[B^p,B^f]], op). rule((A v B)^t, [[A^t,B^t]], ot). tex_rn(of, ["{", bslash, "lor}", bslash, "colon f"]). tex_rn(op, ["{", bslash, "lor}", bslash, "colon p"]). tex_rn(ot, ["{", bslash, "lor}", bslash, "colon t"]). % Negation % %op(500, fx, -). tex_op((-A), [bslash, "neg", A]). rule((-A)^f, [[A^t]], nf). rule((-A)^p, [[A^p]], np). rule((-A)^t, [[A^f]], nt). tex_rn(nf, ["{", bslash, "neg}", bslash, "colon f"]). tex_rn(np, ["{", bslash, "neg}", bslash, "colon p"]). tex_rn(nt, ["{", bslash, "neg}", bslash, "colon t"]). % Test sequents % ts(s1, [(a=>b)^p, (a v c)^t]). ts(s2, [(a=>(b=>a))^t]). ts(s3, [(a&b)^f, a^p, (a v b)^t]). ts(s4, [(a&b)^f, (a&b)^p, b^t]). ts(s5, [(((a =>b) => b) => ((b => a) => a))^t]). tex_opname(a, ["A"]). tex_opname(b, ["B"]). tex_opname(c, ["C"]).