Propositional Logic checker using the list monad for backtracking.

Backtracking.hs

module Backtracking where

-- https://www.ps.uni-saarland.de/~duchier/python/continuations.html

import Prelude hiding (and, not, or)

data Formula
    = Var Int
    | Not Formula
    | And Formula Formula
    | Or Formula Formula
    deriving Show

type Binding = [(Int, Bool)]

satisfy :: Binding -> Formula -> [Binding]
satisfy bindings (Var v) =
    case lookup v bindings of
        Just True  -> [bindings]
        Just False -> []
        Nothing    -> [(v, True) : bindings]
satisfy bindings (Not p)   = falsify bindings p
satisfy bindings (And p q) = satisfy bindings p >>= (`satisfy` q)
satisfy bindings (Or p q)  = satisfy bindings p ++ satisfy bindings q

falsify :: Binding -> Formula -> [Binding]
falsify bindings (Var v) =
    case lookup v bindings of
        Just True  -> []
        Just False -> [bindings]
        Nothing    -> [(v, False) : bindings]
falsify bindings (Not p)   = satisfy bindings p
falsify bindings (And p q) = falsify bindings p ++ falsify bindings q
falsify bindings (Or p q)  = falsify bindings p >>= (`falsify` q)

prove :: Formula -> Bool
prove = null . falsify []

and :: Formula -> Formula -> Formula
and = And

or :: Formula -> Formula -> Formula
or = Or

not :: Formula -> Formula
not = Not

(~>) :: Formula -> Formula -> Formula
p ~> q = or (not p) q

infixr 6 ~>

(<~>) :: Formula -> Formula -> Formula
p <~> q = (p ~> q) `and` (q ~> p)

infixr 5 <~>

p, q, r, s :: Formula
p = Var 0
q = Var 1
r = Var 2
s = Var 3

-- Pelletier, Francis Jeffry. 1986. Seventy-Five Problems for Testing Automatic
-- Theorem Provers.
--
-- prove $ (p ~> q) <~> (not q ~> not p)
-- prove $ not (not p) ~> p
-- prove $ not (p ~> q) ~> (q ~> p)
-- prove $ (not p ~> q) <~> (not q ~> p)
-- prove $ (p `or` q ~> p `or` r) ~> p `or` (q ~> r)
-- prove $ p `or` not p
-- prove $ p `or` not (not (not p))
-- prove $ ((p ~> q) ~> p) ~> p
-- prove $ (p `or` q) `and` (not p `or` q) `and` (p `or` not q) ~> not (not p `or` not q)
-- prove $ (p ~> r) `and` (r ~> p `and` q) `and` p ~> (q `or` r) ~> (p <~> q)
-- prove $ p <~> p
-- prove $ ((p <~> q) <~> r) <~> (p <~> (q <~> r))
-- prove $ p `or` (q `and` r) <~> (p `or` q) `and` (p `or` r)
-- prove $ (p <~> q) <~> (q `or` not p) `and` (not q `or` p)
-- prove $ (p ~> q) <~> not p `or` q
-- prove $ (p ~> q) `or` (q ~> p)
-- prove $ (p `and` (q ~> r) ~> s) <~> (not p `or` q `or` s) `and` (not p `or` not r `or` s)