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

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)```

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

• Dr. Syntaxfree

Dr. Syntaxfree has no PhD and shouldn't call himself a "doctor", but does so for amusement value anyway. An unemployed (ok, graduate student) econopundit by day, he's been progressively obsessed about Haskell to the point he often can't fathom not working on it. A jack-of-many-trades, he has an unusual CS background in that he knows no imperative programming at all, he hopes to be both helpful to those less knowledgeable than him and illustrative to the really smart people trying to understand the mentality of a common man trying to tackle functional programming.