Copyright	(c) Rene Wagner Klaus Luettich Uni Bremen 2005-2007
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable (imports Logic)
Safe Haskell	None

SoftFOL.Logic_SoftFOL

Contents

Orphan instances

Description

Instance of class Logic for SoftFOL.

Synopsis

data SoftFOL = SoftFOL

Documentation

data SoftFOL Source #

A dummy datatype for the LogicGraph and for identifying the right instances

Constructors

SoftFOL

Instances

Instances details

Show SoftFOL Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods showsPrec :: Int -> SoftFOL -> ShowS show :: SoftFOL -> String showList :: [SoftFOL] -> ShowS
Language SoftFOL Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods language_name :: SoftFOL -> String Source # description :: SoftFOL -> String Source #
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence Source # simplify_sen :: SoftFOL -> Sign -> Sentence -> Sentence Source # negation :: SoftFOL -> Sentence -> Maybe Sentence Source # print_sign :: SoftFOL -> Sign -> Doc Source # print_named :: SoftFOL -> Named Sentence -> Doc Source # sym_of :: SoftFOL -> Sign -> [Set SFSymbol] Source # mostSymsOf :: SoftFOL -> Sign -> [SFSymbol] Source # symmap_of :: SoftFOL -> SoftFOLMorphism -> EndoMap SFSymbol Source # sym_name :: SoftFOL -> SFSymbol -> Id Source # sym_label :: SoftFOL -> SFSymbol -> Maybe String Source # fullSymName :: SoftFOL -> SFSymbol -> String Source # symKind :: SoftFOL -> SFSymbol -> String Source # symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol] Source # pair_symbols :: SoftFOL -> SFSymbol -> SFSymbol -> Result SFSymbol 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 #
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source # stability :: SoftFOL -> Stability Source # data_logic :: SoftFOL -> Maybe AnyLogic Source # top_sublogic :: SoftFOL -> () Source # all_sublogics :: SoftFOL -> [()] Source # bottomSublogic :: SoftFOL -> Maybe () Source # sublogicDimensions :: SoftFOL -> [[()]] Source # parseSublogic :: SoftFOL -> String -> Maybe () Source # proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source # provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source # default_prover :: SoftFOL -> String Source # cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source # conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source # empty_proof_tree :: SoftFOL -> ProofTree Source # syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: SoftFOL -> Maybe OMCD Source # export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source # export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source # omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #
Syntax SoftFOL [TPTP] SFSymbol () () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parsersAndPrinters :: SoftFOL -> Map String (PrefixMap -> AParser st [TPTP], [TPTP] -> Doc) Source # parse_basic_spec :: SoftFOL -> Maybe (PrefixMap -> AParser st [TPTP]) Source # parseSingleSymbItem :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: SoftFOL -> [TPTP] -> Item Source # symb_items_name :: SoftFOL -> () -> [String] Source #
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Orphan instances

Pretty Sign Source #
Instance details Methods pretty :: Sign -> Doc Source # pretties :: [Sign] -> Doc Source #