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)
About these ads


7 Responses to “This might or might not qualify as a theorem prover”

  1. 1 augustss

    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

  2. 2 augustss

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

  3. 3 syntaxfree (on the run)

    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!

  4. Modus ponens:

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

    Modus tollens:

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

  5. 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

  6. 6 ChristianS

    “(==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.

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


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


Follow

Get every new post delivered to your Inbox.

%d bloggers like this: