| Copyright | (c) Eugen Kuksa, Uni Bremen 2011 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | eugenk@informatik.uni-bremen.de |
| Stability | experimental |
| Portability | non-portable (via Logic.Logic) |
| Safe Haskell | Safe-Inferred |
CommonLogic.Sublogic
Description
Sublogics for CommonLogic
- sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
- data CLTextType
- data CommonLogicSL = CommonLogicSL {
- format :: CLTextType
- compact :: Bool
- sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
- top :: CommonLogicSL
- bottom :: CommonLogicSL
- propsl :: CommonLogicSL
- folsl :: CommonLogicSL
- fullclsl :: CommonLogicSL
- sublogics_all :: [CommonLogicSL]
- sublogics_name :: CommonLogicSL -> String
- sl_sig :: CommonLogicSL -> Sign -> CommonLogicSL
- sl_sym :: CommonLogicSL -> Symbol -> CommonLogicSL
- sl_mor :: CommonLogicSL -> Morphism -> CommonLogicSL
- sl_symmap :: CommonLogicSL -> SYMB_MAP_ITEMS -> CommonLogicSL
- sl_symitems :: CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL
- sublogic_text :: CommonLogicSL -> TEXT -> CommonLogicSL
- sublogic_name :: CommonLogicSL -> NAME -> CommonLogicSL
- prSymbolM :: CommonLogicSL -> Symbol -> Maybe Symbol
- prSig :: CommonLogicSL -> Sign -> Sign
- prMor :: CommonLogicSL -> Morphism -> Morphism
- prSymMapM :: CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
- prSymItemsM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
- prName :: CommonLogicSL -> NAME -> Maybe NAME
- prBasicSpec :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
Documentation
sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
determines sublogic for basic spec
data CLTextType
types of sublogics
Constructors
| Propositional | Text without quantifiers |
| FirstOrder | Text in First Order Logic |
| Impredicative |
data CommonLogicSL
sublogics for CommonLogic
Constructors
| CommonLogicSL | |
Fields
| |
Instances
sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
Yields the greater sublogic
top :: CommonLogicSL
Greates sublogc: FullCommonLogic
Smallest sublogic: Propositional
Propositional as Sublogic
FirstOrder as Sublogic
sublogics_all :: [CommonLogicSL]
all sublogics
sublogics_name :: CommonLogicSL -> String
String representation of a Sublogic
sl_sig :: CommonLogicSL -> Sign -> CommonLogicSL
determines the sublogic for a Signature
sl_sym :: CommonLogicSL -> Symbol -> CommonLogicSL
determines the sublogic for symbols
sl_mor :: CommonLogicSL -> Morphism -> CommonLogicSL
determines the sublogic for a morphism
sl_symmap :: CommonLogicSL -> SYMB_MAP_ITEMS -> CommonLogicSL
determines the sublogic for symbol map items
sl_symitems :: CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL
determines sublogc for symb items
sublogic_text :: CommonLogicSL -> TEXT -> CommonLogicSL
determines the sublogic for a complete text
sublogic_name :: CommonLogicSL -> NAME -> CommonLogicSL
determines the sublogic for names, ignoring predicates
prSymbolM :: CommonLogicSL -> Symbol -> Maybe Symbol
projection of a symbol to a sublogic
prSig :: CommonLogicSL -> Sign -> Sign
projection of a signature to a sublogic
prMor :: CommonLogicSL -> Morphism -> Morphism
projection of a morphism to a sublogic
prSymMapM :: CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projection of symb map items to a sublogic
prSymItemsM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prName :: CommonLogicSL -> NAME -> Maybe NAME
projection of a name to a sublogic
prBasicSpec :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
filters all TEXTs inside the BASIC_SPEC of which the sublogic is less than
or equal to cs