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.

moduleMainwhereimportData.ListimportData.Maybe -- ExpressionsdataExpr a = LSym a | LNot (Expr a) | (Expr a):&(Expr a) | (Expr a):|(Expr a) | (Expr a):->(Expr a)deriving(Show, Eq) -- Minimal core languagedataCExpr 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) =letisConj x =casexof(CAnd_) -> True;_-> False conj = find isConj ts terms = delete (fromJust conj) tsincaseconjofNothing -> 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))wheresimplifyAnd (CAnd t) (CAnd t') = CAnd (t ++ t') simplifyAnd (CAnd t) x = CAnd (t ++ [x]) simplify (COr terms) = foldl simplifyOr (COr []) (map simplify (sort terms))wheresimplifyOr (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 =ife' == etheneelseresolve e'wheree' = (toCNF . simplify . reduce) e -- Resolution patterns -- (P or A or ...) and (~P or B or ...) ==> (A or B or ...) reduce (CAnd terms) =letunify [] = [] unify (t:t1:xs) =casemerge t t1ofJust e -> unify (e:xs) Nothing ->let(first:rest) = unify (t:xs)infirst:unify (t1:rest) unify (x:xs) = x:unify xs terms' = map reduce (nub terms)inCAnd (unify (deleteFirstsBy (==) terms' [COr [], CAnd []])) -- P or ~P or A ==> [] and P or P ==> P reduce (COr terms) = COr (map reduce (nub (nontrivial terms)))wherenontrivial [] = [] nontrivial (x:xs) =ifany (isNot x) xsthen[]elsex: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) =letcancel []_= [] cancel (x:xs) ys =casefind (isNot x) ysofNothing -> cancel xs ys Just e -> x:cancel xs (delete e ys)incasecancel t1 t2of[] -> 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)) ++ ")"

## 2 Comments

How are things?

Depends, who’s asking?