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
Data.Syntaxfree 
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 ……………………