Copyright | (c) Dominik Luecke, Uni Bremen 2007 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | luecke@informatik.uni-bremen.de |
Stability | experimental |
Portability | portable Definition of morphisms for temporal logic copied from "Propositional.Morphism" Ref. Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser. 2005. |
Safe Haskell | Safe-Inferred |
- data Morphism = Morphism {}
- pretty :: Pretty a => a -> Doc
- idMor :: Sign -> Morphism
- isLegalMorphism :: Morphism -> Result ()
- composeMor :: Morphism -> Morphism -> Result Morphism
- inclusionMap :: Sign -> Sign -> Morphism
- mapSentence :: Morphism -> FORMULA -> Result FORMULA
- mapSentenceH :: Morphism -> FORMULA -> FORMULA
- applyMap :: Map Id Id -> Id -> Id
- applyMorphism :: Morphism -> Id -> Id
Documentation
data Morphism
The datatype for morphisms in temporal logic as maps of sets
Eq Morphism | |
Ord Morphism | |
Show Morphism | |
ShATermConvertible Morphism | |
Pretty Morphism | |
Typeable * Morphism | |
Category Sign Morphism | Instance of Category for temporal logic |
Sentences Temporal FORMULA Sign Morphism Symbol | Instance of Sentences for temporal logic |
StaticAnalysis Temporal BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol | Static Analysis for propositional logic |
Logic Temporal () BASIC_SPEC FORMULA () () Sign Morphism Symbol Symbol () | Instance of Logic for propositional logc |
isLegalMorphism :: Morphism -> Result ()
Determines whether a morphism is valid
composeMor :: Morphism -> Morphism -> Result Morphism
Composition of morphisms in temporal Logic
inclusionMap :: Sign -> Sign -> Morphism
Inclusion map of a subsig into a supersig
mapSentence :: Morphism -> FORMULA -> Result FORMULA
sentence translation along signature morphism here just the renaming of formulae
mapSentenceH :: Morphism -> FORMULA -> FORMULA
applyMorphism :: Morphism -> Id -> Id
Application funtion for morphisms