> module Inferences where > import Theorem > import List Here are some examples of writing your own inference rules, using only the primitive inference rules. Some of them also illustrates how to use the "do" syntactic sugar and the monadic nature of Maybe to make error-handling look like exception handling (more like exception ignoring) in conventional languages. > disch_all t = if (hyp t == []) then t > else disch_all \$ disch (head (hyp t)) t > disch_all2 t = p `mplus` return t > where p = if null (hyp t) then mzero :: Maybe Theorem > else do let x = disch (head (hyp t)) t > disch_all2 x > undisch t | isImp c = mp t (assume (sub1 c)) > | otherwise = Nothing > where c = concl t > add_assum term thm = just \$ mp (disch term thm) (assume term) > conj_elim_all :: Theorem -> [Theorem] > conj_elim_all t = just (conj_elimS t []) > where conj_elimS :: Theorem -> [Theorem] -> Maybe [Theorem] > conj_elimS t ts = p `mplus` return (t:ts) > where p = do (x,y) <- conj_elim t > conj_elimS x =<< conj_elimS y ts > -- sample inference: a ==> b ==> c |- a && b ==> c > Just thm1 = do let t1 = assume (parse "a ==> b ==> c") > t3 = assume (parse "a && b") > (t4,t5) <- conj_elim t3 > t6 <- mp t1 t4 > t7 <- mp t6 t5 > return (disch (parse "a && b") t7) > -- another example: a && b ==> c |- a ==> b ==> c > Just thm2 = do let t1 = assume (parse "a && b ==> c") > t2 = conj_intro (assume\$parse "a", assume\$parse "b") > t3 <- mp t1 t2 > return (disch (parse "a") (disch (parse "b") t3))