Hets - the Heterogeneous Tool Set
Copyright (c) Dominik Luecke Uni Bremen 2007 GPLv2 or higher, see LICENSE.txt luecke@informatik.uni-bremen.de experimental portable Definition of morphisms for propositional logic copied to "Temporal.Morphism" Ref. Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser. 2005. Safe

Propositional.Morphism

Description

Synopsis

# Documentation

data Morphism Source #

The datatype for morphisms in propositional logic as maps of sets

Constructors

 Morphism Fieldssource :: Sign target :: Sign propMap :: Map Id Id

#### Instances

Instances details
 Eq Morphism Source # Instance detailsDefined in Propositional.Morphism Methods(==) :: Morphism -> Morphism -> Bool(/=) :: Morphism -> Morphism -> Bool Data Morphism Source # Instance detailsDefined in Propositional.Morphism Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphismgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MorphismtoConstr :: Morphism -> ConstrdataTypeOf :: Morphism -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Morphism)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)gmapT :: (forall b. Data b => b -> b) -> Morphism -> MorphismgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> rgmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> Morphism -> m MorphismgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m MorphismgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism Ord Morphism Source # Instance detailsDefined in Propositional.Morphism Methodscompare :: Morphism -> Morphism -> Ordering(<) :: Morphism -> Morphism -> Bool(<=) :: Morphism -> Morphism -> Bool(>) :: Morphism -> Morphism -> Bool(>=) :: Morphism -> Morphism -> Bool Show Morphism Source # Instance detailsDefined in Propositional.Morphism MethodsshowsPrec :: Int -> Morphism -> ShowSshow :: Morphism -> StringshowList :: [Morphism] -> ShowS Generic Morphism Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep Morphism :: Type -> Type Methodsfrom :: Morphism -> Rep Morphism xto :: Rep Morphism x -> Morphism FromJSON Morphism Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser MorphismparseJSONList :: Value -> Parser [Morphism] ToJSON Morphism Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: Morphism -> ValuetoEncoding :: Morphism -> EncodingtoJSONList :: [Morphism] -> ValuetoEncodingList :: [Morphism] -> Encoding ShATermConvertible Morphism Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> Morphism -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [Morphism] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism)fromShATermList' :: Int -> ATermTable -> (ATermTable, [Morphism]) Source # Instance detailsDefined in Propositional.Morphism Methodspretties :: [Morphism] -> Doc Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance of Category for propositional logic Instance detailsDefined in Propositional.Logic_Propositional MethodsisInclusion :: Morphism -> Bool Source # Source # Instance of Sentences for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsnegation :: Propositional -> FORMULA -> Maybe FORMULA Source #sym_of :: Propositional -> Sign -> [Set Symbol] Source #sym_label :: Propositional -> Symbol -> Maybe String Source #fullSymName :: Propositional -> Symbol -> String Source #symKind :: Propositional -> Symbol -> String Source # Source # Static Analysis for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsbasic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #matches :: Propositional -> Symbol -> Symbol -> Bool Source #is_subsig :: Propositional -> Sign -> Sign -> Bool Source #is_transportable :: Propositional -> Morphism -> Bool Source #is_injective :: Propositional -> Morphism -> Bool Source #corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source #mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: QBF2Prop -> Bool Source #is_weakly_amalgamable :: QBF2Prop -> Bool Source #constituents :: QBF2Prop -> [String] Source #isInclusionComorphism :: QBF2Prop -> Bool Source #rps :: QBF2Prop -> Bool Source #eps :: QBF2Prop -> Bool Source #isGTC :: QBF2Prop -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source #mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #has_model_expansion :: Prop2QBF -> Bool Source #is_weakly_amalgamable :: Prop2QBF -> Bool Source #constituents :: Prop2QBF -> [String] Source #isInclusionComorphism :: Prop2QBF -> Bool Source #rps :: Prop2QBF -> Bool Source #eps :: Prop2QBF -> Bool Source #isGTC :: Prop2QBF -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source #mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source #mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep Morphism Instance detailsDefined in Propositional.ATC_Propositional type Rep Morphism = D1 ('MetaData "Morphism" "Propositional.Morphism" "main" 'False) (C1 ('MetaCons "Morphism" 'PrefixI 'True) (S1 ('MetaSel ('Just "source") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sign) :*: (S1 ('MetaSel ('Just "target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sign) :*: S1 ('MetaSel ('Just "propMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id Id)))))

pretty :: Pretty a => a -> Doc Source #

Constructs an id-morphism

Determines whether a morphism is valid

Composition of morphisms in propositional Logic

Inclusion map of a subsig into a supersig

sentence translation along signature morphism here just the renaming of formulae

applyMap :: Map Id Id -> Id -> Id Source #

Application function for propMaps

Application funtion for morphisms