Proof.hs revision 3d13c5135e7bab987599acf23afe9c59df49b06f
b66914021bd429f41311d2909a7e9289866da7fdndmodule Proof
b51bf223f42d43ca6b1b33c95124edcfa5a871a4nd-- ((-->), (<-->), (\/), (/\), true, false, box, dia, neg, var, provable)
b66914021bd429f41311d2909a7e9289866da7fdndimport Data.List (delete, intersect, nub)
031b91a62d25106ae69d4693475c79618dd5e884fielding-- data type for fomulas
031b91a62d25106ae69d4693475c79618dd5e884fieldingdata Form = Var Int |
031b91a62d25106ae69d4693475c79618dd5e884fielding Not !Form | -- �A
031b91a62d25106ae69d4693475c79618dd5e884fielding Box !Form | -- [] A
031b91a62d25106ae69d4693475c79618dd5e884fielding Conj !Form !Form -- A/\B
b66914021bd429f41311d2909a7e9289866da7fdnd deriving (Eq)
b66914021bd429f41311d2909a7e9289866da7fdndtype Sequent = [Form] -- defines a sequent
b66914021bd429f41311d2909a7e9289866da7fdnd-- pretty printing (sort of)
b66914021bd429f41311d2909a7e9289866da7fdndinstance Show Form where
b66914021bd429f41311d2909a7e9289866da7fdnd show (Var p) = "p" ++ (show p)
b66914021bd429f41311d2909a7e9289866da7fdnd show (Not p) = "~" ++ show p
b66914021bd429f41311d2909a7e9289866da7fdnd show (Box p) = "[]" ++ show p
b66914021bd429f41311d2909a7e9289866da7fdnd show (Conj p q) = "(" ++ show p ++ " & " ++ show q ++ ")"
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- syntactic sugar
eed2a23d9b5986937f1e2b1c120be97744508a72nd(-->) :: Form -> Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndinfixr 5 -->
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- p --> q = Disj (Not p) q
eed2a23d9b5986937f1e2b1c120be97744508a72ndp --> q = Not (Conj p (Not q))
eed2a23d9b5986937f1e2b1c120be97744508a72nd(<-->) :: Form -> Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndinfixr 4 <-->
eed2a23d9b5986937f1e2b1c120be97744508a72ndp <--> q = Not (Conj (Not ( Conj p q)) (Not(Conj (Not p) (Not q))))
eed2a23d9b5986937f1e2b1c120be97744508a72ndbox :: Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndbox p = Box p
eed2a23d9b5986937f1e2b1c120be97744508a72nddia :: Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72nddia p = Not( Box ( Not p ) )
eed2a23d9b5986937f1e2b1c120be97744508a72nd(/\) :: Form -> Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndp /\ q = Conj p q
eed2a23d9b5986937f1e2b1c120be97744508a72nd(\/) :: Form -> Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndp \/ q = neg ( (neg p) /\ (neg q))
eed2a23d9b5986937f1e2b1c120be97744508a72ndneg :: Form -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndneg p = Not p
eed2a23d9b5986937f1e2b1c120be97744508a72ndfalse :: Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndfalse = (Var 0) /\ (Not (Var 0))
eed2a23d9b5986937f1e2b1c120be97744508a72ndtrue :: Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndtrue = neg false
eed2a23d9b5986937f1e2b1c120be97744508a72ndvar :: Int -> Form
eed2a23d9b5986937f1e2b1c120be97744508a72ndvar n = Var n
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- the rank of a modal formula
eed2a23d9b5986937f1e2b1c120be97744508a72ndrank :: Form -> Int
eed2a23d9b5986937f1e2b1c120be97744508a72ndrank (Box p) = 1 + (rank p)
eed2a23d9b5986937f1e2b1c120be97744508a72ndrank (Conj p q) = (max (rank p) (rank q))
eed2a23d9b5986937f1e2b1c120be97744508a72ndrank (Not p) = rank p
f5e4573f2a3ca4b7d7d10bfb50950fa7eff27efbnilgunrank (Var p) = 0
f5e4573f2a3ca4b7d7d10bfb50950fa7eff27efbnilgun-- expand applies all sequent rules that do not induce branching
f5e4573f2a3ca4b7d7d10bfb50950fa7eff27efbnilgunexpand :: Sequent -> Sequent
eed2a23d9b5986937f1e2b1c120be97744508a72ndexpand s | seq s $ False = undefined -- force strictness
eed2a23d9b5986937f1e2b1c120be97744508a72ndexpand [] = []
eed2a23d9b5986937f1e2b1c120be97744508a72ndexpand ((Not (Not p)):as) = expand (p:as)
eed2a23d9b5986937f1e2b1c120be97744508a72ndexpand ((Not (Conj p q)):as) = expand ((Not p):(Not q):as)
eed2a23d9b5986937f1e2b1c120be97744508a72ndexpand (a:as) = a:(expand as)
eed2a23d9b5986937f1e2b1c120be97744508a72nd----------------------------------------------------------------------------------------------------
eed2a23d9b5986937f1e2b1c120be97744508a72nd--Inference Rules
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- map a sequent the list of all lists of all premises that derive
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- the sequent. Note that a premise is a list of sequents:
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- * to prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- * to prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- * to prove A, neg A, Gamma we need no premises
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- So a premise is a list of sequents, and the list of all possible
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- premises therefore has type [[ Sequent ]]
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- the functions below compute the list of all possible premises
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- that allow to derive a given sequent using the rule that
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- lends its name to the function.
4930be147adf9e3f6d3ca9313a6524f9bf654b2dndaxiom :: Sequent -> [[Sequent]]
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- faster to check for atomic axioms
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- axiom1 xs = [ [] | p <- xs, (Not q) <- xs, p==q]
eed2a23d9b5986937f1e2b1c120be97744508a72ndaxiom xs = nub [ [] | (Var n) <- xs, (Not (Var m)) <- xs, m==n]
eed2a23d9b5986937f1e2b1c120be97744508a72ndnegI :: Sequent -> [[Sequent]]
eed2a23d9b5986937f1e2b1c120be97744508a72ndnegI xs = [ [(p: delete f xs)] | f@(Not(Not p)) <- xs]
eed2a23d9b5986937f1e2b1c120be97744508a72ndnegConj :: Sequent -> [[Sequent]]
eed2a23d9b5986937f1e2b1c120be97744508a72ndnegConj (as) = [[( (Not(p)): (Not(q)) : delete f as )]| f@(Not(Conj p q)) <- as]
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- two variants here: use @-patterns or ``plain'' recursion.
eed2a23d9b5986937f1e2b1c120be97744508a72ndconj :: Sequent -> [[ Sequent ]]
eed2a23d9b5986937f1e2b1c120be97744508a72ndconj s | seq s $ False = undefined -- force strictness
eed2a23d9b5986937f1e2b1c120be97744508a72ndconj (as) = [ [ (p: delete f as) , ( q: delete f as )] | f@(Conj p q ) <- as]
bcf004854091600aa279525d6772e1827114d39dndboxI :: Sequent -> [[Sequent]]
9963f91528694fb21e93da8584c31f226c6de97akessboxI (xs) = let as = [ (Not p) | (Not(Box p)) <- xs]
eed2a23d9b5986937f1e2b1c120be97744508a72nd in [ [ p:as] | (Box p) <- xs ] ++
eed2a23d9b5986937f1e2b1c120be97744508a72nd [ [ (Not q):delete g xs] | g@(Not (Box q)) <- xs ] -- T rule
b51bf223f42d43ca6b1b33c95124edcfa5a871a4ndtRule :: Sequent -> [[ Sequent ]]
b51bf223f42d43ca6b1b33c95124edcfa5a871a4ndtRule (xs) = [ [ (Not p):delete f xs] | f@(Not (Box p)) <- xs ] -- T rule
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- collect all possible premises, i.e. the union of the possible
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- premises taken over the set of all rules in one to get the
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- recursion off the ground.
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- CAVEAT: the order of axioms /rules has a HUGE impact on performance.
eed2a23d9b5986937f1e2b1c120be97744508a72ndallRules :: Sequent -> [[Sequent]]
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- this is as good as it gets if we apply the individual rules
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- message for the afterworld: if you want to find proofs quickly,
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- first look at the rules that induce branching.
b51bf223f42d43ca6b1b33c95124edcfa5a871a4nd-- allRules s = (axiom1 s) ++ (axiom2 s) ++ (boxI s) ++ (conj s) ++ (negDisj s) ++ (negI s) ++ (negConj s) ++ (disj s)
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- we can do slightly better if we apply all rules that do not
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- induce branching in one single step.
eed2a23d9b5986937f1e2b1c120be97744508a72ndallRules s = let t = expand s in (axiom $ t) ++ (boxI $ t) ++ (conj $ t) -- ++ (tRule t)
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- A sequent is provable iff there exists a set of premises that
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- prove the sequent such that all elements in the list of premises are
4930be147adf9e3f6d3ca9313a6524f9bf654b2dnd-- themselves provable.
eed2a23d9b5986937f1e2b1c120be97744508a72ndsprovable :: Sequent -> Bool
eed2a23d9b5986937f1e2b1c120be97744508a72ndsprovable s | seq s $ False = undefined -- force strictness
eed2a23d9b5986937f1e2b1c120be97744508a72ndsprovable s = any (\p -> (all sprovable p)) (allRules s)
eed2a23d9b5986937f1e2b1c120be97744508a72nd-- specialisatino to formulas
eed2a23d9b5986937f1e2b1c120be97744508a72ndprovable :: Form -> Bool
eed2a23d9b5986937f1e2b1c120be97744508a72ndprovable p = sprovable [ p ]
b3ab5b870526aebe7da94a01350677b5087fc26and-- test cases:
b3ab5b870526aebe7da94a01350677b5087fc26anddp1 = (neg (neg p)) \/ ((neg (neg q)) \/ r) -- not provable
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp2 = box p \/ neg(box p) -- provable
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp3 = box p \/ neg(box(neg(neg p))) -- provable
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp4 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ neg(box q))
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp5 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ dia(neg q))
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp6 = (box p) /\ (dia q) --> (dia (p /\ q)) -- true?
f1110149b5b6c28ecc39d1958d98ad9cfa8e41f3nddp7 = (box (dia (box p))) --> (dia (box (neg p))) -- false?
eed2a23d9b5986937f1e2b1c120be97744508a72ndlevel :: Int -> [Form]
eed2a23d9b5986937f1e2b1c120be97744508a72ndlevel 0 = [var 0, var 1, neg $ var 0, neg $ var 1 ]