Contents Index

MultiKnowledge.KFormula

Description

Knowledge formulas with LTL and LLP.

Synopsis

data KFormula = Var Variable | Not KFormula | And KFormula KFormula | Or KFormula KFormula | Impl KFormula KFormula | Nec KFormula | Forall Variable KFormula | Forall_i Int Variable KFormula | Next KFormula | Until KFormula KFormula | Prev KFormula | Since KFormula KFormula | Eventually KFormula type Variable = String kFormulaToIsabelle :: KFormula -> IO IsabelleFile

Documentation

data KFormula

Constructors Var Variable Not KFormula And KFormula KFormula Or KFormula KFormula Impl KFormula KFormula Nec KFormula Forall Variable KFormula Forall_i Int Variable KFormula Next KFormula Until KFormula KFormula Prev KFormula Since KFormula KFormula Eventually KFormula Instances Eq KFormula Interfaced KFormula Provable KFormula Show KFormula Solve KFormula Typeable KFormula Check KFormula IsabelleFile

type Variable = String

Propositional variables

kFormulaToIsabelle :: KFormula -> IO IsabelleFile

Produced by Haddock version 0.8