Logic_CommonLogic.hs revision 3831cf8a3b0ea144a80d13fe0314cc2752e32107
51846950b4b1f31342008cf17f667859a5f21949Christian MaederModule : $Header$
51846950b4b1f31342008cf17f667859a5f21949Christian MaederDescription : Instance of class Logic for propositional logic
51846950b4b1f31342008cf17f667859a5f21949Christian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
51846950b4b1f31342008cf17f667859a5f21949Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
51846950b4b1f31342008cf17f667859a5f21949Christian MaederMaintainer : luecke@informatik.uni-bremen.de
51846950b4b1f31342008cf17f667859a5f21949Christian MaederStability : experimental
51846950b4b1f31342008cf17f667859a5f21949Christian MaederPortability : non-portable (imports Logic.Logic)
51846950b4b1f31342008cf17f667859a5f21949Christian MaederInstance of class Logic for the propositional logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder Also the instances for Syntax and Category.
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder http://en.wikipedia.org/wiki/Propositional_logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder What is a Logic?.
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder-- | Lid for propositional logic
51846950b4b1f31342008cf17f667859a5f21949Christian Maederdata CommonLogic = CommonLogic deriving Show
51846950b4b1f31342008cf17f667859a5f21949Christian Maederinstance Language CommonLogic where
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder description _ = "CommonLogic Logic\n"
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder ++ "for more information please refer to\n"
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder ++ "http://en.wikipedia.org/wiki/Propositional_logic"
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederdata Sign = Sign
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder-- | Instance of Category derived by default
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder-- | Instance of Sentences for propositional logic
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Sentences CommonLogic SENTENCE Sign (DefaultMorphism Sign) ()
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder negation CommonLogic = Just . negateFormula
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder -- returns the set of symbols
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder sym_of CommonLogic = symOf
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder -- returns the symbol map
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder symmap_of CommonLogic = getSymbolMap
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder -- returns the name of a symbol
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder sym_name CommonLogic = getSymbolName
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder -- translation of sentences along signature morphism
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder map_sen CommonLogic = mapSentence
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder -- there is nothing to leave out
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder simplify_sen CommonLogic _ = simplify
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder-- | Syntax of CommonLogic logic
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Syntax CommonLogic [SENTENCE] () ()
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder parse_basic_spec CommonLogic = Just basicSpec
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder parse_symb_items CommonLogic = Just symbItems
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder parse_symb_map_items CommonLogic = Just symbMapItems
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder-- | Instance of Logic for propositional logc
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance Logic CommonLogic
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder () -- Sublogics
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder [SENTENCE] -- basic_spec
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder SENTENCE -- sentence
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder () -- symb_items
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder () -- symb_map_items
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder (DefaultMorphism Sign) -- morphism
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder () -- raw_symbol
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder () -- proof_tree
51846950b4b1f31342008cf17f667859a5f21949Christian Maeder-- | Static Analysis for propositional logic
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maederinstance StaticAnalysis CommonLogic
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder [SENTENCE] -- basic_spec
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder SENTENCE -- sentence
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder (DefaultMorphism Sign)
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder basic_analysis CommonLogic =
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder Just basicCommonLogicAnalysis
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder empty_signature CommonLogic = emptySig
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder is_subsig CommonLogic = isSubSigOf
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder subsig_inclusion CommonLogic s = return . inclusionMap s
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder signature_union CommonLogic = sigUnion
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder symbol_to_raw CommonLogic = symbolToRaw
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder id_to_raw CommonLogic = idToRaw
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder matches CommonLogic = Symbol.matches
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder stat_symb_items CommonLogic = mkStatSymbItems
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder stat_symb_map_items CommonLogic = mkStatSymbMapItem
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder morphism_union CommonLogic = morphismUnion
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder induced_from_morphism CommonLogic = inducedFromMorphism
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder induced_from_to_morphism CommonLogic = inducedFromToMorphism
3831cf8a3b0ea144a80d13fe0314cc2752e32107Christian Maeder signature_colimit CommonLogic = signatureColimit