Hets - the Heterogeneous Tool Set
Copyright (c) Jonathan von Schroeder DFKI GmbH 2010 GPLv2 or higher, see LICENSE.txt experimental portable Safe

QBF.Morphism

Description

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.

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 QBF.Morphism Methods(==) :: Morphism -> Morphism -> Bool(/=) :: Morphism -> Morphism -> Bool Data Morphism Source # Instance detailsDefined in QBF.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 QBF.Morphism Methodscompare :: Morphism -> Morphism -> Ordering(<) :: Morphism -> Morphism -> Bool(<=) :: Morphism -> Morphism -> Bool(>) :: Morphism -> Morphism -> Bool(>=) :: Morphism -> Morphism -> Bool Show Morphism Source # Instance detailsDefined in QBF.Morphism MethodsshowsPrec :: Int -> Morphism -> ShowSshow :: Morphism -> StringshowList :: [Morphism] -> ShowS Generic Morphism Instance detailsDefined in QBF.ATC_QBF Associated Typestype Rep Morphism :: Type -> Type Methodsfrom :: Morphism -> Rep Morphism xto :: Rep Morphism x -> Morphism FromJSON Morphism Instance detailsDefined in QBF.ATC_QBF MethodsparseJSON :: Value -> Parser MorphismparseJSONList :: Value -> Parser [Morphism] ToJSON Morphism Instance detailsDefined in QBF.ATC_QBF MethodstoJSON :: Morphism -> ValuetoEncoding :: Morphism -> EncodingtoJSONList :: [Morphism] -> ValuetoEncodingList :: [Morphism] -> Encoding ShATermConvertible Morphism Instance detailsDefined in QBF.ATC_QBF 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 QBF.Morphism Methodspretties :: [Morphism] -> Doc Source # Source # Instance detailsDefined in QBF.Logic_QBF Methods Source # Instance detailsDefined in QBF.Logic_QBF Methods Source # Instance of Category for propositional logic Instance detailsDefined in QBF.Logic_QBF MethodsisInclusion :: Morphism -> Bool Source # Source # Instance of Sentences for propositional logic Instance detailsDefined in QBF.Logic_QBF Methodsnegation :: QBF -> FORMULA -> Maybe FORMULA Source #sym_of :: QBF -> Sign -> [Set Symbol] Source #mostSymsOf :: QBF -> Sign -> [Symbol] Source #sym_label :: QBF -> Symbol -> Maybe String Source #fullSymName :: QBF -> Symbol -> String Source #symKind :: QBF -> Symbol -> String Source #symsOfSen :: QBF -> Sign -> FORMULA -> [Symbol] Source # Source # Static Analysis for propositional logic Instance detailsDefined in QBF.Logic_QBF Methodsbasic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source #stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source #convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source #ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source #matches :: QBF -> Symbol -> Symbol -> Bool Source #is_subsig :: QBF -> Sign -> Sign -> Bool Source #generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source #is_transportable :: QBF -> Morphism -> Bool Source #is_injective :: QBF -> Morphism -> Bool Source #corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in QBF.Logic_QBF Methodsparse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source #data_logic :: QBF -> Maybe AnyLogic Source #all_sublogics :: QBF -> [QBFSL] Source #bottomSublogic :: QBF -> Maybe QBFSL Source #sublogicDimensions :: QBF -> [[QBFSL]] Source #parseSublogic :: QBF -> String -> Maybe QBFSL Source #default_prover :: QBF -> String Source #syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: QBF -> Maybe OMCD Source #export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL 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 # type Rep Morphism Instance detailsDefined in QBF.ATC_QBF type Rep Morphism = D1 ('MetaData "Morphism" "QBF.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