Propositional Logic checker.

Bool.hs

module Bool where

-- THIS LOGIC CHECKER IS INCORRECT. FOR A CORRECT ONE SEE:
-- https://gist.github.com/pedrominicz/d72b88b190298beb0ecf2a9ed09acb81

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

import Control.Monad.State
import Data.IntMap

import Prelude hiding (and, lookup, not, or)

type Binding = IntMap Bool

class Formula a where
    satisfy :: a -> State Binding Bool
    falsify :: a -> State Binding Bool

data Not p = Not p

instance Formula p => Formula (Not p) where
    satisfy (Not p) = falsify p
    falsify (Not p) = satisfy p

data And p q = And p q

instance (Formula p, Formula q) => Formula (And p q) where
    satisfy (And p q) = do
        p <- satisfy p
        q <- satisfy q
        return $ p && q

    falsify (And p q) = do
        p <- falsify p
        q <- falsify q
        return $ p || q

data Or p q = Or p q

instance (Formula p, Formula q) => Formula (Or p q) where
    satisfy (Or p q) = falsify (And (Not p) (Not q))
    falsify (Or p q) = satisfy (And (Not p) (Not q))

data Variable = Variable Int

assign :: Bool -> Variable -> State Binding Bool
assign value (Variable var) = do
    bindings <- get
    case lookup var bindings of
        Just value'
            | value == value' -> return True
            | otherwise       -> return False
        Nothing -> do
            modify (insert var value)
            return True

instance Formula Variable where
    satisfy = assign True
    falsify = assign False

prove :: Formula a => a -> Bool
prove formula =
    case evalState (falsify formula) empty of
        True  -> False
        False -> True

and :: p -> q -> And p q
and = And

or :: p -> q -> Or p q
or = Or

not :: p -> Not p
not = Not

type Impl p q = Or (Not p) q

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

infixr 6 ~>

(<~>) :: p -> q -> And (Impl p q) (Impl q p)
p <~> q = and (p ~> q) (q ~> p)

infixr 5 <~>

p, q, r :: Variable
p = Variable 0
q = Variable 1
r = Variable 2

{-
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 q `or` q
prove $ (p ~> q) `or` (q ~> p)
-}