Copyright	(c) Jonathan von Schroeder, DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	<jonathan.von_schroeder@dfki.de>
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred

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

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 QBFSL Morphism
MinSublogic QBFSL Morphism
Category Sign Morphism	Instance of Category for propositional logic
Sentences QBF FORMULA Sign Morphism Symbol	Instance of Sentences for propositional logic
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol	Static Analysis for propositional logic
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS 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

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