Proof.hs revision 81c09542d31779a407196fbd710aa8e69a815522
842ae4bd224140319ae7feec1872b93dfd491143fieldingmodule Proof where
842ae4bd224140319ae7feec1872b93dfd491143fielding-- ((-->), (<-->), (\/), (/\), true, false, box, dia, neg, var, provable)
842ae4bd224140319ae7feec1872b93dfd491143fieldingimport Data.List (delete, intersect, nub)
842ae4bd224140319ae7feec1872b93dfd491143fielding-- data type for fomulas
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdata Form = Var Int --Var Char (Maybe Int) -- variables
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes | Not !Form -- �A
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes | Box !Form -- [] A
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes | Conj !Form !Form -- A/\B
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes deriving (Eq)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestype Sequent = [Form] -- defines a sequent
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- pretty printing (sort of)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesinstance Show Form where
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes show f = case f of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Var i -> "p" ++ show i
e8f95a682820a599fe41b22977010636be5c2717jim Not g -> "~" ++ show g
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Box g -> "[]" ++ show g
e8f95a682820a599fe41b22977010636be5c2717jim Conj g h -> "(" ++ show g ++ "&" ++ show h ++ ")"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- syntactic sugar
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes(-->) :: Form -> Form -> Form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesp --> q = Not (Conj p (Not q)) -- ~p\/q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes(<-->) :: Form -> Form -> Form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesinfixr 4 <-->
5c0419d51818eb02045cf923a9fe456127a44c60wrowep <--> q = Conj (p-->q) (q-->p) --Not (Conj (Not (Conj p q)) (Not(Conj (Not p) (Not q))))
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesbox :: Form -> Form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesbox p = Box p
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdia :: Form -> Form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdia p = Not(Box(Not p))
d266c3777146d36a4c23c17aad6f153aebea1bf4jorton(/\) :: Form -> Form -> Form
d266c3777146d36a4c23c17aad6f153aebea1bf4jortonp /\ q = Conj p q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes(\/) :: Form -> Form -> Form
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesp \/ q = neg ((neg p) /\ (neg q))
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesneg :: Form -> Form
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesneg p = Not p
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesfalse :: Form
22f8da8087791fcb95b836c8a81937c5a9bba202bnicholesfalse = (Var 0) /\ (Not (Var 0))
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestrue = neg false
0568280364eb026393be492ebc732795c4934643jortonvar :: Int -> Form
0568280364eb026393be492ebc732795c4934643jortonvar n = Var n
0568280364eb026393be492ebc732795c4934643jorton-- the rank of a modal formula
0568280364eb026393be492ebc732795c4934643jortonrank :: Form -> Int
0568280364eb026393be492ebc732795c4934643jortonrank (Box p) = 1 + (rank p)
0568280364eb026393be492ebc732795c4934643jortonrank (Conj p q) = (max (rank p) (rank q))
0568280364eb026393be492ebc732795c4934643jortonrank (Not p) = rank p
0568280364eb026393be492ebc732795c4934643jortonrank (Var p) = 0
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- expand applies all sequent rules that do not induce branching
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand :: Sequent -> Sequent
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand s | seq s $ False = undefined -- force strictness
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand [] = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand ((Not (Not p)):as) = expand (p:as)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand ((Not (Conj p q)):as) = expand ((Not p):(Not q):as)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexpand (a:as) = a:(expand as)
796e4a7141265d8ed7036e4628161c6eafb2a789jorton----------------------------------------------------------------------------------------------------
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes--Inference Rules
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- map a sequent the list of all lists of all premises that derive
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the sequent. Note that a premise is a list of sequents:
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- * to prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- * to prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- * to prove A, neg A, Gamma we need no premises
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- So a premise is a list of sequents, and the list of all possible
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- premises therefore has type [[ Sequent ]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the functions below compute the list of all possible premises
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- that allow to derive a given sequent using the rule that
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- lends its name to the function.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesaxiom :: Sequent -> [[Sequent]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- faster to check for atomic axioms
8113dac419143273351446c3ad653f3fe5ba5cfdwrowe-- axiom1 xs = [ [] | p <- xs, (Not q) <- xs, p==q]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesaxiom xs = nub [ [] | (Var n) <- xs, (Not (Var m)) <- xs, m==n]
e8f95a682820a599fe41b22977010636be5c2717jimnegI :: Sequent -> [[Sequent]]
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowenegI xs = [ [(p: delete f xs)] | f@(Not(Not p)) <- xs]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnegConj :: Sequent -> [[Sequent]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnegConj (as) = [[( (Not(p)): (Not(q)) : delete f as )]| f@(Not(Conj p q)) <- as]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- two variants here: use @-patterns or ``plain'' recursion.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesconj :: Sequent -> [[ Sequent ]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesconj s | seq s $ False = undefined -- force strictness
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesconj (as) = [ [ (p: delete f as) , ( q: delete f as )] | f@(Conj p q ) <- as]
713a2b68bac4aeb1e9c48785006c0732451039depquernaboxI :: Sequent -> [[Sequent]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesboxI (xs) = let as = [ (Not p) | (Not(Box p)) <- xs]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in [ [ p:as] | (Box p) <- xs ] ++
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes [ [ (Not q):delete g xs] | g@(Not (Box q)) <- xs ] -- T rule
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestRule :: Sequent -> [[ Sequent ]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestRule (xs) = [ [ (Not p):delete f xs] | f@(Not (Box p)) <- xs ] -- T rule
482f676c6c19b1c5bb5cca04dad11509c1da3a4cwrowe-- collect all possible premises, i.e. the union of the possible
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- premises taken over the set of all rules in one to get the
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- recursion off the ground.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- CAVEAT: the order of axioms /rules has a HUGE impact on performance.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesallRules :: Sequent -> [[Sequent]]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- this is as good as it gets if we apply the individual rules
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- message for the afterworld: if you want to find proofs quickly,
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- first look at the rules that induce branching.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- allRules s = (axiom1 s) ++ (axiom2 s) ++ (boxI s) ++ (conj s) ++ (negDisj s) ++ (negI s) ++ (negConj s) ++ (disj s)
f43b67c5a9d29b572eac916f8335cedc80c908bebnicholes-- we can do slightly better if we apply all rules that do not
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- induce branching in one single step.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesallRules s = let t = expand s in (axiom $ t) ++ (boxI $ t) ++ (conj $ t) -- ++ (tRule t)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- A sequent is provable iff there exists a set of premises that
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- prove the sequent such that all elements in the list of premises are
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- themselves provable.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessprovable :: Sequent -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessprovable s | seq s $ False = undefined -- force strictness
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessprovable s = any (\p -> (all sprovable p)) (allRules s)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- specialisatino to formulas
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesprovable :: Form -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesprovable p = sprovable [ p ]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- test cases:
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp1 = (neg (neg p)) \/ ((neg (neg q)) \/ r) -- not provable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp2 = box p \/ neg(box p) -- provable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp3 = box p \/ neg(box(neg(neg p))) -- provable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp4 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ neg(box q))
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp5 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ dia(neg q))
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp6 = (box p) /\ (dia q) --> (dia (p /\ q)) -- true?
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdp7 = (box (dia (box p))) --> (dia (box (neg p))) -- false?
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslevel :: Int -> [Form]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslevel 0 = [var 0, var 1, neg $ var 0, neg $ var 1 ]
8113dac419143273351446c3ad653f3fe5ba5cfdwrowelevel n = let pbox = map box [ x | i <- [0 .. (n-1)], x <- (level i)]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nbox = map (neg . box) [ x | i <- [0 .. (n-1)], x <- (level i)]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pbox ++ nbox ++ [ p /\ q | p <- pbox, q <- nbox] ++ [neg (p /\ q) | p <- pbox, q <- nbox ]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestforms :: [ (Sequent, Sequent) ]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestforms = [ ([neg a, neg $ box a, b ], [neg $ box a, b]) | a <- level 2, b <- level 2]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesttest :: [ (Sequent, Sequent) ] -> String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesttest [] = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesttest ( (s1, s2):as ) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let s1p = (sprovable s1) ;
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s2p = (sprovable s2)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in if (s1p /= s2p) then "GOTCHA: " ++ (show s1) ++ (show s2) ++ "<"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else "*" ++ (ttest as)