### This might or might not qualify as a theorem prover

13Jun07

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)

Filed under: Uncategorized | 7 Comments

It’s some kind of theorem prover.

Do you have some future expansion in mind that made you parametrize Formula?

BTW, a simplification:

truth (a :-> b) = not (truth a) || truth b

BTW, you can write an overloaded taut that works for any number of arguments.

Well, yeah. This is the “Mortality of Socrates” theorem:

*Main> taut3 (\s h m -> ((h :-> m) :* (s :-> h)) :-> (s :-> m))

True

Yay my first theorem prover!

Modus ponens:

*Main> taut2 $ \a b -> ((a :-> b) :* a) :-> b

True

Modus tollens:

*Main> taut2 $ \a b -> ((a :-> b) :* a) :-> b

True

Oops. Modus tollens:

*Main> taut2 $ \fire oxygen -> (( fire:-> oxygen) :* (Not oxygen)) :-> (Not fire)

True

Affirming the consequent:

*Main> taut2 $ \f o -> (( f:-> o) :* o) :-> f

False

Denying the antecedent:

*Main> taut2 $ \f o -> (( f:-> o) :* o) :-> f

False

False syllogism:

*Main> taut3 $ \socrates cat mortal -> ((cat :-> mortal) :* (socrates :-> mortal)) :-> socrates :-> cat

False

“(==True)” is the same as “id”,

“all (==True)” is the same as “and”,

“all (==False)” is “not . any”.

“consistent” seems wrong with the possibility to give two different arities.

HELOO IM SANDRA

how are you doing dear one ,you jast wounder who sent you this message it that so dont worry mine name is sandra ,but you can call me jassica ,that is the way mine friends call me ,im in close to here from yuou if you can dall inlove with you and maybe not gonna be anything hard for you ,im single and not to be close with too much men but i am interesting with ur profile and i wish if maybe you can be interesting with mine profile too dear ,it hard to bilieve unless we chart each orther then ,ok im sexy and like to talk alot lol sorry but that is mine behaviour not anything but i think you can change me if we meet in our charting ,how are you doing mine dear im kool out here and you did you have a good day ,as i has the same way to meet you and for real you and i sandra from Africa ,mine dear one i has to go now so catch you later after your reply ……………………