b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuModule : $EmptyHeader$
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuDescription : <optional short description entry>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuCopyright : (c) <Authors or Affiliations>
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuMaintainer : <email>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuStability : unstable | experimental | provisional | stable | frozen
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuPortability : portable | non-portable (<reason>)
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu<optional description>
81c09542d31779a407196fbd710aa8e69a815522Georgel Calinmodule Proof where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ((-->), (<-->), (\/), (/\), true, false, box, dia, neg, var, provable)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinimport Data.List (delete, intersect, nub)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- data type for fomulas
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Form = Var Int -- Var Char (Maybe Int) -- variables
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Not !Form -- ¬A
05d4bb01e11ad19f2efb41a3efec59a7784c9942Christian Maeder | Box !Form -- [] A
05d4bb01e11ad19f2efb41a3efec59a7784c9942Christian Maeder | Conj !Form !Form -- A/\B
81c09542d31779a407196fbd710aa8e69a815522Georgel Calin deriving (Eq)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype Sequent = [Form] -- defines a sequent
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- pretty printing (sort of)
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian Maederinstance Show Form where
81c09542d31779a407196fbd710aa8e69a815522Georgel Calin show f = case f of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Var i -> 'p' : show i
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Not g -> '~' : show g
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Box g -> "[]" ++ show g
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Conj g h -> '(' : show g ++ "&" ++ show h ++ ")"
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- syntactic sugar
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian Maeder(-->) :: Form -> Form -> Form
81c09542d31779a407196fbd710aa8e69a815522Georgel Calinp --> q = Not (Conj p (Not q)) -- ~p\/q
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian Maeder(<-->) :: Form -> Form -> Form
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederp <--> q = Conj (p --> q) (q --> p)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- Not (Conj (Not (Conj p q)) (Not(Conj (Not p) (Not q))))
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinbox :: Form -> Form
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian Maederdia :: Form -> Form
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdia p = Not (Box (Not p))
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin(/\) :: Form -> Form -> Form
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinp /\ q = Conj p q
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin(\/) :: Form -> Form -> Form
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederp \/ q = neg (neg p /\ neg q)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinneg :: Form -> Form
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederfalse = Var 0 /\ Not (Var 0)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calintrue = neg false
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinvar :: Int -> Form
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- the rank of a modal formula
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinrank :: Form -> Int
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederrank (Box p) = 1 + rank p
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederrank (Conj p q) = max (rank p) (rank q)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinrank (Not p) = rank p
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinrank (Var p) = 0
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- expand applies all sequent rules that do not induce branching
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinexpand :: Sequent -> Sequent
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexpand s | seq s False = undefined -- force strictness
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinexpand [] = []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexpand (Not (Not p) : as) = expand (p : as)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexpand (Not (Conj p q) : as) = expand (Not p : Not q : as)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexpand (a : as) = a : expand as
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- Inference Rules
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermap a sequent the list of all lists of all premises that derive
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthe sequent. Note that a premise is a list of sequents:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederto prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederto prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederto prove A, neg A, Gamma we need no premises
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederSo a premise is a list of sequents, and the list of all possible
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederpremises therefore has type [[ Sequent ]] -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- the functions below compute the list of all possible premises
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthat allow to derive a given sequent using the rule that
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederlends its name to the function. -}
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinaxiom :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- faster to check for atomic axioms
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederaxiom1 xs = [ [] | p <- xs, (Not q) <- xs, p==q] -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederaxiom xs = nub [ [] | (Var n) <- xs, (Not (Var m)) <- xs, m == n]
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian MaedernegI :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernegI xs = [ [p : delete f xs] | f@(Not (Not p)) <- xs]
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian MaedernegConj :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernegConj as = [ [Not p : Not q : delete f as] | f@(Not (Conj p q)) <- as]
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- two variants here: use @-patterns or ``plain'' recursion.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconj :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconj s | seq s False = undefined -- force strictness
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconj (as) = [ [p : delete f as, q : delete f as] | f@(Conj p q) <- as]
902bfaac7e88afebb6684fe1f2414ae2efbc7edfChristian MaederboxI :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederboxI (xs) = let as = [ Not p | Not (Box p) <- xs]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in [ [ p : as] | Box p <- xs ] ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [ [ Not q : delete g xs ] | g@(Not (Box q)) <- xs ] -- T rule
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel CalintRule :: Sequent -> [[ Sequent ]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertRule xs = [ [ Not p : delete f xs ] | f@(Not (Box p)) <- xs ] -- T rule
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- collect all possible premises, i.e. the union of the possible
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederpremises taken over the set of all rules in one to get the
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederrecursion off the ground. -}
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- CAVEAT: the order of axioms /rules has a HUGE impact on performance.
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel CalinallRules :: Sequent -> [[Sequent]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- this is as good as it gets if we apply the individual rules
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermessage for the afterworld: if you want to find proofs quickly,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederfirst look at the rules that induce branching.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederallRules s = (axiom1 s) ++ (axiom2 s) ++ (boxI s) ++ (conj s) ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder(negDisj s) ++ (negI s) ++ (negConj s) ++ (disj s) -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- we can do slightly better if we apply all rules that do not
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinduce branching in one single step. -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederallRules s = let t = expand s in axiom t ++ boxI t ++ conj t -- ++ (tRule t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- A sequent is provable iff there exists a set of premises that
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederprove the sequent such that all elements in the list of premises are
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthemselves provable. -}
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinsprovable :: Sequent -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersprovable s | seq s False = undefined -- force strictness
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersprovable s = any (all sprovable) (allRules s)
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calin-- specialisatino to formulas
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinprovable :: Form -> Bool
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinprovable p = sprovable [ p ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp1 = neg (neg p) \/ (neg (neg q) \/ r) -- not provable
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp2 = box p \/ neg (box p) -- provable
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp3 = box p \/ neg (box (neg (neg p))) -- provable
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp4 = neg ( neg (box p /\ neg (box p)) --> (box q /\ box p) /\ neg (box q))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp5 = neg ( neg (box p /\ neg (box p)) --> (box q /\ box p) /\ dia (neg q))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp6 = box p /\ dia q --> dia (p /\ q) -- true?
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdp7 = box (dia (box p)) --> dia (box (neg p)) -- false?
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinlevel :: Int -> [Form]
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinlevel 0 = [var 0, var 1, neg $ var 0, neg $ var 1 ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederlevel n = let pbox = map box [ x | i <- [0 .. n - 1], x <- level i]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nbox = map (neg . box) [ x | i <- [0 .. n - 1], x <- level i]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in pbox ++ nbox ++ [ p /\ q | p <- pbox, q <- nbox] ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [neg (p /\ q) | p <- pbox, q <- nbox ]
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calintforms :: [ (Sequent, Sequent) ]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertforms = [ ([neg a, neg $ box a, b ], [neg $ box a, b]) |
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a <- level 2, b <- level 2]
3d13c5135e7bab987599acf23afe9c59df49b06fGeorgel Calinttest :: [ (Sequent, Sequent) ] -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederttest ( (s1, s2) : as ) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let s1p = sprovable s1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s2p = sprovable s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if s1p /= s2p then "GOTCHA: " ++ show s1 ++ show s2 ++ "<"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else '*' : ttest as