Immanence

This might or might not qualify as a theorem prover

Just been implementing sentential logic as I progress through the textbook.

module Main where
import Control.Monad

data Formula a =
			 Prim a
			 | (Formula a) :+ (Formula a)
			 | (Formula a) :* (Formula a)
			 | (Formula a) :-> (Formula a)
			 | Not (Formula a) deriving Show

(<->)  :: (Formula a) -> (Formula a) -> (Formula a)
a <-> b = (a :-> b)  :* (b :-> a)
inv (a :-> b) = b :-> a

showP (a,b) = show a ++ "====>" ++ show b ++ "n"
showF = putStr . unlines . map showP . map (k->(k, truth k))

bools =  fmap Prim [True, False]

arity1 f = map f bools
arity2 f = liftM2 f bools bools
arity3 f = liftM3 f bools bools bools

solve arity f = map truth (arity f)

taut1 f = all (==True) (solve arity1 f)
taut2 f = all (==True) (solve arity2 f)
taut3 f = all (==True) (solve arity3 f)

contr1 f = all (==False) (solve arity1 f)
contr2 f = all (==False) (solve arity2 f)
contr3 f = all (==False) (solve arity3 f)

conting1 f = (not (taut1 f)) && (not (contr1 f))
conting2 f = (not (taut2 f)) && (not (contr2 f))
conting3 f = (not (taut3 f)) && (not (contr3 f))

equiv1 f g = all (==True) (zipWith (==) (solve arity1 f) (solve arity1 g))
equiv2 f g = all (==True) (zipWith (==) (solve arity2 f) (solve arity2 g))
equiv3 f g = all (==True) (zipWith (==) (solve arity3 f) (solve arity3 g))

consistent arity1 f arity2 g = any (==True) (zipWith (&&) (solve arity1 f) (solve arity2 g))

conseq prem1 prem2 concl = ((prem1 :* prem2) :-> concl)

truth :: (Formula Bool) -> Bool
truth (Prim z) = z
truth (a :+ b) = (truth a) || (truth b)
truth (a :* b) = (truth a) && (truth b)
truth (Not a) = not (truth a)
truth (a :-> b) = ((truth a) == (truth b)) || (truth a == False)

-- some examples
-- to print a truth table, use
-- showF $ arityN example
-- where arityN depends on the number of arguments.
-- or use tautN, contrN, etc. ex: taut1 lem

lem x = (Not (Not x)) <-> x
xor x y = (x :* (Not y)) :+ ((Not x) :* y)
hiti a b = (a :* b) :-> b
gligli a b = (a :+ b) <-> (b :+ b)
compli c = ((c <-> c) :-> c) :* (Not (c :-> c))
minv m n p = m :* (n :+ p)

© 2007 μ = m // dayvan cowboy // music is math ↵.