16 structure Prop :> PROP = 17 struct 18 datatype prop = 19 Atom of string 20 | True 21 | And of prop * prop 22 | False 23 | Or of prop * prop 24 | Implies of prop * prop 25 26 fun Not A = Implies (A, False) 27 28 fun toStringImp (Implies (A, B)) = toStringAndOr A ^ " => " ^ toStringImp B 29 | toStringImp A = toStringAndOr A 30 31 and toStringAndOr (And (A, B)) = toStringAtomic A ^ " & " ^ toStringAtomic B 32 | toStringAndOr (Or (A, B)) = toStringAtomic A ^ " | " ^ toStringAtomic B 33 | toStringAndOr A = toStringAtomic A 34 35 and toStringAtomic (Atom s) = s 36 | toStringAtomic True = "T" 37 | toStringAtomic False = "F" 38 | toStringAtomic A = "(" ^ toStringImp A ^ ")" 39 40 fun toString x = toStringImp x 41 end 42 43 signature G4IP = 44 sig 45 (* [decide A = true] iff . ===> A has a proof, 46 [decide A = false] iff . ===> A has no proof *) 47 val decide : Prop.prop -> bool 48 end 49 50 structure G4ip :> G4IP = 51 struct 52 structure P = Prop 53 54 (* g is gammer, the context for noninvertible dudes. 55 * w is ohmigger, the context for invertible dudes. *) 56 57 (* decideleft does invertible left rules 58 * the 'true/false' is whether or not to check for atom in the context. 59 * whenever we do a recursive call when adding to w, need to say true. *) 60 (* init *) 61 fun decidel true g w (Atom(s)) =