module LogicTest import Logic // Some random examples e1 = Atom 'p' e2 = Atom 'q' e3 = App1 Not e1 e4 = App2 e1 And e2 e5 = App2 e3 Or e2 e6 = App2 e3 Impl e3 e7 = App2 e4 Equiv e5 e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q') e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q')) exprs_rand = [e1,e2,e3,e4,e5,e6,e7,e8,e9] // To test associativity rules e10 = App2 (App2 (Atom 'p') And (Atom 'q')) And (Atom 'r') e11 = App2 (Atom 'p') And (App2 (Atom 'q') And (Atom 'r')) e12 = App2 (App2 (Atom 'p') Or (Atom 'q')) Or (Atom 'r') e13 = App2 (Atom 'p') Or (App2 (Atom 'q') Or (Atom 'r')) e14 = App2 (App2 (Atom 'p') Impl (Atom 'q')) Impl (Atom 'r') e15 = App2 (Atom 'p') Impl (App2 (Atom 'q') Impl (Atom 'r')) e16 = App2 (App2 (Atom 'p') Equiv (Atom 'q')) Equiv (Atom 'r') e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r')) exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17] //Start = map all_atom_options exprs_rand //Start = toString (all_atom_options e4) //Start = substitute ('q',True) e8 table = { exprs = exprs_rand ++ exprs_assoc, options = all_atom_options e4 } Start = toString table