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

CommonLogic.Sublogic

Description

Sublogics for CommonLogic

Synopsis

sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
data CLTextType
- = Propositional
- | FirstOrder
- | Impredicative
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 Source #

determines sublogic for basic spec

data CLTextType Source #

types of sublogics

Constructors

Propositional	Text without quantifiers
FirstOrder	Text in First Order Logic
Impredicative

Instances

Instances details

Bounded CLTextType Source #
Instance details Defined in CommonLogic.Sublogic Methods minBound :: CLTextType maxBound :: CLTextType
Enum CLTextType Source #
Instance details Defined in CommonLogic.Sublogic Methods succ :: CLTextType -> CLTextType pred :: CLTextType -> CLTextType toEnum :: Int -> CLTextType fromEnum :: CLTextType -> Int enumFrom :: CLTextType -> [CLTextType] enumFromThen :: CLTextType -> CLTextType -> [CLTextType] enumFromTo :: CLTextType -> CLTextType -> [CLTextType] enumFromThenTo :: CLTextType -> CLTextType -> CLTextType -> [CLTextType]
Eq CLTextType Source #
Instance details Defined in CommonLogic.Sublogic Methods (==) :: CLTextType -> CLTextType -> Bool (/=) :: CLTextType -> CLTextType -> Bool
Ord CLTextType Source #
Instance details Defined in CommonLogic.Sublogic Methods compare :: CLTextType -> CLTextType -> Ordering (<) :: CLTextType -> CLTextType -> Bool (<=) :: CLTextType -> CLTextType -> Bool (>) :: CLTextType -> CLTextType -> Bool (>=) :: CLTextType -> CLTextType -> Bool max :: CLTextType -> CLTextType -> CLTextType min :: CLTextType -> CLTextType -> CLTextType
Show CLTextType Source #
Instance details Defined in CommonLogic.Sublogic Methods showsPrec :: Int -> CLTextType -> ShowS show :: CLTextType -> String showList :: [CLTextType] -> ShowS
Generic CLTextType
Instance details Defined in CommonLogic.ATC_CommonLogic Associated Types type Rep CLTextType :: Type -> Type Methods from :: CLTextType -> Rep CLTextType x to :: Rep CLTextType x -> CLTextType
FromJSON CLTextType
Instance details Defined in CommonLogic.ATC_CommonLogic Methods parseJSON :: Value -> Parser CLTextType parseJSONList :: Value -> Parser [CLTextType]
ToJSON CLTextType
Instance details Defined in CommonLogic.ATC_CommonLogic Methods toJSON :: CLTextType -> Value toEncoding :: CLTextType -> Encoding toJSONList :: [CLTextType] -> Value toEncodingList :: [CLTextType] -> Encoding
ShATermConvertible CLTextType
Instance details Defined in CommonLogic.ATC_CommonLogic Methods toShATermAux :: ATermTable -> CLTextType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CLTextType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CLTextType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CLTextType])
type Rep CLTextType
Instance details Defined in CommonLogic.ATC_CommonLogic type Rep CLTextType = D1 ('MetaData "CLTextType" "CommonLogic.Sublogic" "main" 'False) (C1 ('MetaCons "Propositional" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FirstOrder" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Impredicative" 'PrefixI 'False) (U1 :: Type -> Type)))

data CommonLogicSL Source #

sublogics for CommonLogic

Constructors

CommonLogicSL
Fields format :: CLTextType compact :: Bool

Instances

Instances details

Eq CommonLogicSL Source #
Instance details Defined in CommonLogic.Sublogic Methods (==) :: CommonLogicSL -> CommonLogicSL -> Bool (/=) :: CommonLogicSL -> CommonLogicSL -> Bool
Ord CommonLogicSL Source #
Instance details Defined in CommonLogic.Sublogic Methods compare :: CommonLogicSL -> CommonLogicSL -> Ordering (<) :: CommonLogicSL -> CommonLogicSL -> Bool (<=) :: CommonLogicSL -> CommonLogicSL -> Bool (>) :: CommonLogicSL -> CommonLogicSL -> Bool (>=) :: CommonLogicSL -> CommonLogicSL -> Bool max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL min :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
Show CommonLogicSL Source #
Instance details Defined in CommonLogic.Sublogic Methods showsPrec :: Int -> CommonLogicSL -> ShowS show :: CommonLogicSL -> String showList :: [CommonLogicSL] -> ShowS
Generic CommonLogicSL
Instance details Defined in CommonLogic.ATC_CommonLogic Associated Types type Rep CommonLogicSL :: Type -> Type Methods from :: CommonLogicSL -> Rep CommonLogicSL x to :: Rep CommonLogicSL x -> CommonLogicSL
FromJSON CommonLogicSL
Instance details Defined in CommonLogic.ATC_CommonLogic Methods parseJSON :: Value -> Parser CommonLogicSL parseJSONList :: Value -> Parser [CommonLogicSL]
ToJSON CommonLogicSL
Instance details Defined in CommonLogic.ATC_CommonLogic Methods toJSON :: CommonLogicSL -> Value toEncoding :: CommonLogicSL -> Encoding toJSONList :: [CommonLogicSL] -> Value toEncodingList :: [CommonLogicSL] -> Encoding
ShATermConvertible CommonLogicSL
Instance details Defined in CommonLogic.ATC_CommonLogic Methods toShATermAux :: ATermTable -> CommonLogicSL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CommonLogicSL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CommonLogicSL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CommonLogicSL])
SublogicName CommonLogicSL Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods sublogicName :: CommonLogicSL -> String Source #
SemiLatticeWithTop CommonLogicSL Source #	Sublogics
Instance details Defined in CommonLogic.Logic_CommonLogic Methods lub :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL Source # top :: CommonLogicSL Source #
ProjectSublogicM CommonLogicSL SYMB_ITEMS Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogicM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS Source #
ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogicM :: CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS Source #
ProjectSublogicM CommonLogicSL NAME Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogicM :: CommonLogicSL -> NAME -> Maybe NAME Source #
ProjectSublogicM CommonLogicSL Symbol Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogicM :: CommonLogicSL -> Symbol -> Maybe Symbol Source #
ProjectSublogic CommonLogicSL BASIC_SPEC Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogic :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC Source #
ProjectSublogic CommonLogicSL Sign Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogic :: CommonLogicSL -> Sign -> Sign Source #
ProjectSublogic CommonLogicSL Morphism Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods projectSublogic :: CommonLogicSL -> Morphism -> Morphism Source #
MinSublogic CommonLogicSL SYMB_ITEMS Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: SYMB_ITEMS -> CommonLogicSL Source #
MinSublogic CommonLogicSL SYMB_MAP_ITEMS Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: SYMB_MAP_ITEMS -> CommonLogicSL Source #
MinSublogic CommonLogicSL NAME Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: NAME -> CommonLogicSL Source #
MinSublogic CommonLogicSL TEXT_META Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: TEXT_META -> CommonLogicSL Source #
MinSublogic CommonLogicSL BASIC_SPEC Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: BASIC_SPEC -> CommonLogicSL Source #
MinSublogic CommonLogicSL Sign Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: Sign -> CommonLogicSL Source #
MinSublogic CommonLogicSL Morphism Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: Morphism -> CommonLogicSL Source #
MinSublogic CommonLogicSL Symbol Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods minSublogic :: Symbol -> CommonLogicSL Source #
Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in CommonLogic.Logic_CommonLogic Methods parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source # stability :: CommonLogic -> Stability Source # data_logic :: CommonLogic -> Maybe AnyLogic Source # top_sublogic :: CommonLogic -> CommonLogicSL Source # all_sublogics :: CommonLogic -> [CommonLogicSL] Source # bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source # sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source # parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source # proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source # provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source # default_prover :: CommonLogic -> String Source # cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source # conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source # empty_proof_tree :: CommonLogic -> ProofTree Source # syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CommonLogic -> Maybe OMCD Source # export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source # export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source # omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source # addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source # addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source # sublogicOfTheo :: CommonLogic -> (Sign, [TEXT_META]) -> CommonLogicSL Source #
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 Source #
Instance details Defined in OWL2.OWL22CommonLogic Methods sourceLogic :: OWL22CommonLogic -> OWL2 Source # sourceSublogic :: OWL22CommonLogic -> ProfSub Source # sourceSublogicLossy :: OWL22CommonLogic -> ProfSub Source # minSourceTheory :: OWL22CommonLogic -> Maybe (LibName, String) Source # targetLogic :: OWL22CommonLogic -> CommonLogic Source # mapSublogic :: OWL22CommonLogic -> ProfSub -> Maybe CommonLogicSL Source # map_theory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: OWL22CommonLogic -> (Sign, [Named Axiom]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: OWL22CommonLogic -> OWLMorphism -> Result Morphism Source # map_sentence :: OWL22CommonLogic -> Sign -> Axiom -> Result TEXT_META Source # map_symbol :: OWL22CommonLogic -> Sign -> Entity -> Set Symbol Source # extractModel :: OWL22CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Axiom]) Source # is_model_transportable :: OWL22CommonLogic -> Bool Source # has_model_expansion :: OWL22CommonLogic -> Bool Source # is_weakly_amalgamable :: OWL22CommonLogic -> Bool Source # constituents :: OWL22CommonLogic -> [String] Source # isInclusionComorphism :: OWL22CommonLogic -> Bool Source # rps :: OWL22CommonLogic -> Bool Source # eps :: OWL22CommonLogic -> Bool Source # isGTC :: OWL22CommonLogic -> Bool Source #
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 Source #
Instance details Defined in Comorphisms.Prop2CommonLogic Methods sourceLogic :: Prop2CommonLogic -> Propositional Source # sourceSublogic :: Prop2CommonLogic -> PropSL Source # sourceSublogicLossy :: Prop2CommonLogic -> PropSL Source # minSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: Prop2CommonLogic -> CommonLogic Source # mapSublogic :: Prop2CommonLogic -> PropSL -> Maybe CommonLogicSL Source # map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: Prop2CommonLogic -> Morphism -> Result Morphism0 Source # map_sentence :: Prop2CommonLogic -> Sign -> FORMULA -> Result TEXT_META Source # map_symbol :: Prop2CommonLogic -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Prop2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: Prop2CommonLogic -> Bool Source # has_model_expansion :: Prop2CommonLogic -> Bool Source # is_weakly_amalgamable :: Prop2CommonLogic -> Bool Source # constituents :: Prop2CommonLogic -> [String] Source # isInclusionComorphism :: Prop2CommonLogic -> Bool Source # rps :: Prop2CommonLogic -> Bool Source # eps :: Prop2CommonLogic -> Bool Source # isGTC :: Prop2CommonLogic -> Bool Source #
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 Source #
Instance details Defined in Comorphisms.CommonLogicModuleElimination Methods sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source # sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source # minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source # targetLogic :: CommonLogicModuleElimination -> CommonLogic Source # mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source # map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source # map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source # map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source # extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CommonLogicModuleElimination -> Bool Source # has_model_expansion :: CommonLogicModuleElimination -> Bool Source # is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source # constituents :: CommonLogicModuleElimination -> [String] Source # isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source # rps :: CommonLogicModuleElimination -> Bool Source # eps :: CommonLogicModuleElimination -> Bool Source # isGTC :: CommonLogicModuleElimination -> Bool Source #
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CommonLogic2IsabelleHOL Methods sourceLogic :: CommonLogic2IsabelleHOL -> CommonLogic Source # sourceSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogic2IsabelleHOL -> CommonLogicSL Source # minSourceTheory :: CommonLogic2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CommonLogic2IsabelleHOL -> Isabelle Source # mapSublogic :: CommonLogic2IsabelleHOL -> CommonLogicSL -> Maybe () Source # map_theory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CommonLogic2IsabelleHOL -> (Sign0, [Named TEXT_META]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CommonLogic2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: CommonLogic2IsabelleHOL -> Sign0 -> TEXT_META -> Result Sentence Source # map_symbol :: CommonLogic2IsabelleHOL -> Sign0 -> Symbol -> Set () Source # extractModel :: CommonLogic2IsabelleHOL -> Sign0 -> () -> Result (Sign0, [Named TEXT_META]) Source # is_model_transportable :: CommonLogic2IsabelleHOL -> Bool Source # has_model_expansion :: CommonLogic2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CommonLogic2IsabelleHOL -> Bool Source # constituents :: CommonLogic2IsabelleHOL -> [String] Source # isInclusionComorphism :: CommonLogic2IsabelleHOL -> Bool Source # rps :: CommonLogic2IsabelleHOL -> Bool Source # eps :: CommonLogic2IsabelleHOL -> Bool Source # isGTC :: CommonLogic2IsabelleHOL -> Bool Source #
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 Source #
Instance details Defined in Comorphisms.CommonLogic2CASL Methods sourceLogic :: CL2CFOL -> CommonLogic Source # sourceSublogic :: CL2CFOL -> CommonLogicSL Source # sourceSublogicLossy :: CL2CFOL -> CommonLogicSL Source # minSourceTheory :: CL2CFOL -> Maybe (LibName, String) Source # targetLogic :: CL2CFOL -> CASL Source # mapSublogic :: CL2CFOL -> CommonLogicSL -> Maybe CASL_Sublogics Source # map_theory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CL2CFOL -> (Sign, [Named TEXT_META]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CL2CFOL -> Morphism -> Result CASLMor Source # map_sentence :: CL2CFOL -> Sign -> TEXT_META -> Result CASLFORMULA Source # map_symbol :: CL2CFOL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: CL2CFOL -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CL2CFOL -> Bool Source # has_model_expansion :: CL2CFOL -> Bool Source # is_weakly_amalgamable :: CL2CFOL -> Bool Source # constituents :: CL2CFOL -> [String] Source # isInclusionComorphism :: CL2CFOL -> Bool Source # rps :: CL2CFOL -> Bool Source # eps :: CL2CFOL -> Bool Source # isGTC :: CL2CFOL -> Bool Source #
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 Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
type Rep CommonLogicSL
Instance details Defined in CommonLogic.ATC_CommonLogic type Rep CommonLogicSL = D1 ('MetaData "CommonLogicSL" "CommonLogic.Sublogic" "main" 'False) (C1 ('MetaCons "CommonLogicSL" 'PrefixI 'True) (S1 ('MetaSel ('Just "format") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CLTextType) :*: S1 ('MetaSel ('Just "compact") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))