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)))
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)) ++ ")"