Hets - the Heterogeneous Tool Set

Copyright(c) Eugen Kuksa, Uni Bremen 2011
LicenseGPLv2 or higher, see LICENSE.txt
Maintainereugenk@informatik.uni-bremen.de
Stabilityexperimental
Portabilitynon-portable (via Logic.Logic)
Safe HaskellSafe-Inferred

CommonLogic.Sublogic

Description

Sublogics for CommonLogic

Synopsis

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

format :: CLTextType
 
compact :: Bool
 

Instances

Eq CommonLogicSL 
Ord CommonLogicSL 
Show CommonLogicSL 
ShATermConvertible CommonLogicSL 
SublogicName CommonLogicSL 
SemiLatticeWithTop CommonLogicSL

Sublogics

Typeable * CommonLogicSL 
ProjectSublogicM CommonLogicSL SYMB_ITEMS 
ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS 
ProjectSublogicM CommonLogicSL NAME 
ProjectSublogicM CommonLogicSL Symbol 
ProjectSublogic CommonLogicSL Sign 
ProjectSublogic CommonLogicSL BASIC_SPEC 
ProjectSublogic CommonLogicSL Morphism 
MinSublogic CommonLogicSL Sign 
MinSublogic CommonLogicSL SYMB_ITEMS 
MinSublogic CommonLogicSL SYMB_MAP_ITEMS 
MinSublogic CommonLogicSL NAME 
MinSublogic CommonLogicSL TEXT_META 
MinSublogic CommonLogicSL BASIC_SPEC 
MinSublogic CommonLogicSL Morphism 
MinSublogic CommonLogicSL Symbol 
Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 
Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 
Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree 
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 

sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL

Yields the greater sublogic

top :: CommonLogicSL

Greates sublogc: FullCommonLogic

bottom :: CommonLogicSL

Smallest sublogic: Propositional

propsl :: CommonLogicSL

Propositional as Sublogic

folsl :: CommonLogicSL

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

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