Copyright | (c) Dominik Luecke, Uni Bremen 2007 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | luecke@informatik.uni-bremen.de |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Basic and static analysis for propositional logic
- basicPropositionalAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
- mkStatSymbItems :: [SYMB_ITEMS] -> Result [Symbol]
- mkStatSymbMapItem :: [SYMB_MAP_ITEMS] -> Result (Map Symbol Symbol)
- inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
- inducedFromToMorphism :: Map Symbol Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
- signatureColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
- pROPsen_analysis :: (BASIC_SPEC, Sign, FORMULA) -> Result FORMULA
Documentation
basicPropositionalAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
mkStatSymbItems :: [SYMB_ITEMS] -> Result [Symbol]
Retrieve raw symbols
mkStatSymbMapItem :: [SYMB_MAP_ITEMS] -> Result (Map Symbol Symbol)
Static analysis for symbol maps
inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
Induce a signature morphism from a source signature and a raw symbol map
inducedFromToMorphism :: Map Symbol Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
Induce a signature morphism from a source signature and a raw symbol map
pROPsen_analysis :: (BASIC_SPEC, Sign, FORMULA) -> Result FORMULA