GenZ-0.1.0.0: lib/Logic/Modal/S4.hs

module Logic.Modal.S4 (sfour) where

import General
import Logic.Modal.K
import Logic.Modal.K4
import Logic.Modal.T
import FormM

sfour :: Logic FormM
sfour = Log { name = "S4"
            , safeRules   = [leftBot, isAxiom, additionRule safeML, boxTrule]
            , unsafeRules = [box4rule]
            }

{-
saturated CPL(safe + local loopcheck) + ☐t rule(safe + local loopcheck) + ☐4 rule(unsafe + global loopcheck):
    φ, □φ, Γ ⇒ ∆
☐t     □φ, Γ ⇒ ∆
       Γ, □Γ ⇒ φ
☐4    Γ', □Γ ⇒ □φ, ∆
-}