Copyright	(c) Dominik Luecke, Uni Bremen 2007
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	experimental
Portability	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 Haskell	Safe-Inferred

Propositional.Morphism

Description

Synopsis

Documentation

data Morphism

The datatype for morphisms in propositional logic as maps of sets

Constructors

Morphism
Fields source :: Sign target :: Sign propMap :: Map Id Id

Instances

Eq Morphism
Data Morphism
Ord Morphism
Show Morphism
ShATermConvertible Morphism
Pretty Morphism
Typeable * Morphism
ProjectSublogic PropSL Morphism
MinSublogic PropSL Morphism
Category Sign Morphism	Instance of Category for propositional logic
Sentences Propositional FORMULA Sign Morphism Symbol	Instance of Sentences for propositional logic
StaticAnalysis Propositional BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol	Static Analysis for propositional logic
Logic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree	Instance of Logic for propositional logc
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS 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 Propositional2OWL2 Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree
Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA 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 CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree

pretty :: Pretty a => a -> Doc

idMor :: Sign -> Morphism

Constructs an id-morphism

isLegalMorphism :: Morphism -> Result ()

Determines whether a morphism is valid

composeMor :: Morphism -> Morphism -> Result Morphism

Composition of morphisms in propositional Logic

inclusionMap :: Sign -> Sign -> Morphism

Inclusion map of a subsig into a supersig

mapSentence :: Morphism -> FORMULA -> Result FORMULA

sentence translation along signature morphism here just the renaming of formulae

mapSentenceH :: Morphism -> FORMULA -> FORMULA

applyMap :: Map Id Id -> Id -> Id

Application function for propMaps

applyMorphism :: Morphism -> Id -> Id

Application funtion for morphisms

morphismUnion :: Morphism -> Morphism -> Result Morphism