Quick and Dirty Theorem Prover.

Wrote a very basic prover for theorems in propositional logic while waiting for a build to finish. Not terribly exciting, but should be relatively easy to extend to first-order logic and/or turn it into a constructive prover by adding a DPLL step. I’ve tested it on a proof by contradiction for the hypothetical syllogism ((a => b) /\ (b => c)) => (a => c), and on some common inference rules. These are the tests:

a = LSym "a"; b = LSym "b"; c = LSym "c"; p = LSym "p"; q = LSym "q"; r = LSym "r"; s = LSym "s"

test = LNot $ ((a :-> b) :& (b :-> c)) :-> (a :-> c)              -- contradiction
test_ModusPonens    = ((p :-> q) :& p)                            -- q
test_ModusTollens   = ((p :-> q) :& (LNot q))                     -- not p
test_HypSyllogism   = ((p :-> q) :& (q :-> r))                    -- p -> r
test_DisSyllogism   = ((p :| q) :& (LNot p))                      -- q
test_ConstrDilemma  = ((p :-> q) :& (r :-> s) :& (p :| r))        -- q or s
test_DestrDilemma   = ((p :-> q) :& (r :-> s) :& ((LNot q) :| (LNot s)))     -- not p or not r

tests = map (pprint . resolve . compile) [test, test_ModusPonens, test_ModusTollens, test_HypSyllogism, test_DisSyllogism, test_ConstrDilemma, test_DestrDilemma]

The algorithm consists of bringing the expression into conjunctive normal form (I’m simultaneously compiling into a desugared core language), and applying a set of resolution steps. The resolution steps consist of trivially rejecting things like A \/ ~A \/ …, simplifying things like A \/ B \/ A \/ …, and merging expressions of the form (P \/ A \/ …) /\ (~P \/ B \/ …) into A \/ B \/ … . The process clearly terminates; when it does, the resulting expression is what has been inferred from the conjecture. If the result is a contradiction, then the conjecture is false, if the result is empty then nothing can be inferred, and if it’s non-empty, then we’ve proven an inference rule.

Obligatory GHCi session:

*Main> pprint (resolve $ compile (LNot $ ((a :-> b) :& (b :-> c)) :-> (a :-> c)))
“(c & ~c)”
*Main> pprint (resolve $ compile ((p :-> q) :& (LNot q)))
“~p”

The code is below. Haven’t run into any bugs, but I haven’t tested it extensively.

module Main where

import Data.List
import Data.Maybe

-- Expressions
data Expr a = LSym a
            | LNot (Expr a)
            | (Expr a) :& (Expr a)
            | (Expr a) :| (Expr a)
            | (Expr a) :-> (Expr a)
            deriving (Show, Eq)

-- Minimal core language
data CExpr a = CSym a
             | CNot (CExpr a)
             | CAnd [CExpr a]
             | COr [CExpr a]
             deriving (Show, Eq, Ord)
             
-- Desugars and transforms to the core language
compile (LSym x)             = CSym x
compile (a :-> b)            = COr [compile $ LNot a, compile b]
compile (LNot a)             = CNot (compile a)
compile (a :| b)             = COr [compile a, compile b]
compile (a :& b)             = CAnd [compile a, compile b]

-- Transforms to CNF
toCNF (CSym a)               = (CSym a)
toCNF (CNot (COr ts))        = toCNF $ CAnd (map CNot ts)
toCNF (CNot (CAnd ts))       = toCNF $ COr (map CNot ts)
toCNF (CNot a)               = CNot (toCNF a)
toCNF (COr ts)               = let
                                      isConj x = case x of (CAnd _) -> True; _ -> False
                                      conj = find isConj ts
                                      terms = delete (fromJust conj) ts
                               in case conj of
                                      Nothing            -> COr (map toCNF ts)
                                      Just (CAnd e)      -> toCNF (CAnd $ map (\t -> COr (t:terms)) e)
toCNF (CAnd ts)              = CAnd (map toCNF ts)

-- Flattens nested connectives, etc.
simplify :: Ord a => CExpr a -> CExpr a
simplify (CAnd [t])          = t
simplify (COr [t])           = t
simplify (CAnd terms)        = foldl simplifyAnd (CAnd []) (map simplify (sort terms))
                               where
                                    simplifyAnd (CAnd t) (CAnd t') = CAnd (t ++ t')
                                    simplifyAnd (CAnd t) x         = CAnd (t ++ [x])

simplify (COr terms)         = foldl simplifyOr (COr []) (map simplify (sort terms))
                               where
                                    simplifyOr (COr t) (COr t')  = COr (t ++ t')
                                    simplifyOr (COr t) x         = COr (t ++ [x])
                                
simplify (CNot (CNot e))     = simplify e
simplify (CNot e)            = CNot (simplify e)
simplify e                   = e


-- Resolution step.  Applies reduction patterns as long as the expression is reducible.
resolve e                    =  if e' == e then e else resolve e'
                                where
                                        e' = (toCNF . simplify . reduce) e
                    
-- Resolution patterns

-- (P or A or ...) and (~P or B or ...) ==> (A or B or ...)
reduce (CAnd terms)          = let
                                    unify [] = []
                                    unify (t:t1:xs) = case merge t t1 of
                                                                    Just e  -> unify (e:xs)
                                                                    Nothing -> let
                                                                                    (first:rest) = unify (t:xs)
                                                                               in
                                                                                    first : unify (t1:rest)
                                    unify (x:xs) = x : unify xs
                                    terms' = map reduce (nub terms)                
                                in
                                    CAnd (unify (deleteFirstsBy (==) terms' [COr [], CAnd []]))

-- P or ~P or A ==> [] and P or P ==> P
reduce (COr terms)           = COr (map reduce (nub (nontrivial terms)))
                               where
                                    nontrivial []       = []
                                    nontrivial (x:xs)   = if any (isNot x) xs then [] else x : nontrivial xs
reduce x                     = x

-- Helper functions
cNot (CNot x) = x
cNot x = CNot x
isNot x y = x == cNot y

-- Merges expressions of the form (P or A or ... ) and (~P or B or ... ) into A or B or ...
merge (COr t1) (COr t2)       = let
                                    cancel [] _         = []
                                    cancel (x:xs) ys    = case find (isNot x) ys of
                                                                Nothing -> cancel xs ys
                                                                Just e  -> x : cancel xs (delete e ys)
                                                                
                                in case cancel t1 t2 of
                                    []          -> Nothing
                                    xs          -> Just (COr $ (t1 \\ xs) ++ (t2 \\ (map cNot xs)))


merge (COr t) e               = merge e (COr t)

merge e (COr t)               = find (isNot e) t >>= \e' -> Just $ COr (delete e' t)

merge e1 e2                   = Nothing


pprint :: CExpr String -> String
pprint (CSym x)         = x
pprint (CNot t)         = "~" ++ pprint t
pprint (COr ts)         = "(" ++ concat (intersperse " | " (map pprint ts)) ++ ")"
pprint (CAnd ts)        = "(" ++ concat (intersperse " & " (map pprint ts)) ++ ")"

About these ads