{- |

Module : $EmptyHeader$

Description : <optional short description entry>

Copyright : (c) <Authors or Affiliations>

License : GPLv2 or higher, see LICENSE.txt

Maintainer : <email>

Stability : unstable | experimental | provisional | stable | frozen

Portability : portable | non-portable (<reason>)

<optional description>

-}

module Proof where

-- ((-->), (<-->), (\/), (/\), true, false, box, dia, neg, var, provable)

import Data.List (delete, intersect, nub)

-- data type for fomulas

data Form = Var Int -- Var Char (Maybe Int) -- variables

| Not !Form -- ¬A

| Box !Form -- [] A

| Conj !Form !Form -- A/\B

deriving (Eq)

type Sequent = [Form] -- defines a sequent

-- pretty printing (sort of)

instance Show Form where

show f = case f of

Var i -> 'p' : show i

Not g -> '~' : show g

Box g -> "[]" ++ show g

Conj g h -> '(' : show g ++ "&" ++ show h ++ ")"

-- syntactic sugar

p = Var 0

q = Var 1

r = Var 2

(-->) :: Form -> Form -> Form

infixr 5 -->

p --> q = Not (Conj p (Not q)) -- ~p\/q

(<-->) :: Form -> Form -> Form

infixr 4 <-->

p <--> q = Conj (p --> q) (q --> p)

-- Not (Conj (Not (Conj p q)) (Not(Conj (Not p) (Not q))))

box :: Form -> Form

box = Box

dia :: Form -> Form

dia p = Not (Box (Not p))

(/\) :: Form -> Form -> Form

infix 7 /\

p /\ q = Conj p q

(\/) :: Form -> Form -> Form

infix 6 \/

p \/ q = neg (neg p /\ neg q)

neg :: Form -> Form

neg = Not

false :: Form

false = Var 0 /\ Not (Var 0)

true :: Form

true = neg false

var :: Int -> Form

var = Var

-- the rank of a modal formula

rank :: Form -> Int

rank (Box p) = 1 + rank p

rank (Conj p q) = max (rank p) (rank q)

rank (Not p) = rank p

rank (Var p) = 0

-- expand applies all sequent rules that do not induce branching

expand :: Sequent -> Sequent

expand s | seq s False = undefined -- force strictness

expand [] = []

expand (Not (Not p) : as) = expand (p : as)

expand (Not (Conj p q) : as) = expand (Not p : Not q : as)

expand (a : as) = a : expand as

-- ------------------------------------------------------------------------------

{- Inference Rules

map a sequent the list of all lists of all premises that derive

the sequent. Note that a premise is a list of sequents:

to prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.

to prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.

to prove A, neg A, Gamma we need no premises

So a premise is a list of sequents, and the list of all possible

premises therefore has type [[ Sequent ]] -}

{- the functions below compute the list of all possible premises

that allow to derive a given sequent using the rule that

lends its name to the function. -}

axiom :: Sequent -> [[Sequent]]

{- faster to check for atomic axioms

axiom1 xs = [ [] | p <- xs, (Not q) <- xs, p==q] -}

axiom xs = nub [ [] | (Var n) <- xs, (Not (Var m)) <- xs, m == n]

negI :: Sequent -> [[Sequent]]

negI xs = [ [p : delete f xs] | f@(Not (Not p)) <- xs]

negConj :: Sequent -> [[Sequent]]

negConj as = [ [Not p : Not q : delete f as] | f@(Not (Conj p q)) <- as]

-- two variants here: use @-patterns or ``plain'' recursion.

conj :: Sequent -> [[Sequent]]

conj s | seq s False = undefined -- force strictness

conj (as) = [ [p : delete f as, q : delete f as] | f@(Conj p q) <- as]

boxI :: Sequent -> [[Sequent]]

boxI (xs) = let as = [ Not p | Not (Box p) <- xs]

in [ [ p : as] | Box p <- xs ] ++

[ [ Not q : delete g xs ] | g@(Not (Box q)) <- xs ] -- T rule

tRule :: Sequent -> [[ Sequent ]]

tRule xs = [ [ Not p : delete f xs ] | f@(Not (Box p)) <- xs ] -- T rule

{- collect all possible premises, i.e. the union of the possible

premises taken over the set of all rules in one to get the

recursion off the ground. -}

-- CAVEAT: the order of axioms /rules has a HUGE impact on performance.

allRules :: Sequent -> [[Sequent]]

{- this is as good as it gets if we apply the individual rules

message for the afterworld: if you want to find proofs quickly,

first look at the rules that induce branching.

allRules s = (axiom1 s) ++ (axiom2 s) ++ (boxI s) ++ (conj s) ++

(negDisj s) ++ (negI s) ++ (negConj s) ++ (disj s) -}

{- we can do slightly better if we apply all rules that do not

induce branching in one single step. -}

allRules s = let t = expand s in axiom t ++ boxI t ++ conj t -- ++ (tRule t)

{- A sequent is provable iff there exists a set of premises that

prove the sequent such that all elements in the list of premises are

themselves provable. -}

sprovable :: Sequent -> Bool

sprovable s | seq s False = undefined -- force strictness

sprovable s = any (all sprovable) (allRules s)

-- specialisatino to formulas

provable :: Form -> Bool

provable p = sprovable [ p ]

-- test cases:

dp1 = neg (neg p) \/ (neg (neg q) \/ r) -- not provable

dp2 = box p \/ neg (box p) -- provable

dp3 = box p \/ neg (box (neg (neg p))) -- provable

dp4 = neg ( neg (box p /\ neg (box p)) --> (box q /\ box p) /\ neg (box q))

dp5 = neg ( neg (box p /\ neg (box p)) --> (box q /\ box p) /\ dia (neg q))

dp6 = box p /\ dia q --> dia (p /\ q) -- true?

dp7 = box (dia (box p)) --> dia (box (neg p)) -- false?

level :: Int -> [Form]

level 0 = [var 0, var 1, neg $ var 0, neg $ var 1 ]

level n = let pbox = map box [ x | i <- [0 .. n - 1], x <- level i]

nbox = map (neg . box) [ x | i <- [0 .. n - 1], x <- level i]

in pbox ++ nbox ++ [ p /\ q | p <- pbox, q <- nbox] ++

[neg (p /\ q) | p <- pbox, q <- nbox ]

tforms :: [ (Sequent, Sequent) ]

tforms = [ ([neg a, neg $ box a, b ], [neg $ box a, b]) |

a <- level 2, b <- level 2]

ttest :: [ (Sequent, Sequent) ] -> String

ttest [] = []

ttest ( (s1, s2) : as ) =

let s1p = sprovable s1

s2p = sprovable s2

in if s1p /= s2p then "GOTCHA: " ++ show s1 ++ show s2 ++ "<"

else '*' : ttest as