Logic_Propositional.hs revision 9a5fda85e9eaf0e6a18d0dd2b8535805c5135e9a
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{-# OPTIONS -cpp #-}
1a6464613c59e35072b90ca296ae402cbe956144Christian MaederModule : $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederDescription : Instance of class Logic for propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (imports Logic.Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederInstance of class Logic for the propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Also the instances for Syntax and Category.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder http://en.wikipedia.org/wiki/Propositional_logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maeder What is a Logic?.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.ATC_Propositional()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.Symbol as Symbol
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.Parse_AS_Basic as Parse_AS
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.Analysis as Analysis
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Propositional.InverseAnalysis as IAna
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersimport qualified Propositional.Sublogic as Sublogic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Common.Id as Id()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder#ifdef UNI_PACKAGE
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersimport qualified Propositional.Prove as Prove
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Lid for propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdata Propositional = Propositional deriving Show --lid
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Language Propositional where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder description _ =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "Propositional Logic\n"++
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "for more information please refer to\n"++
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers "http://en.wikipedia.org/wiki/Propositional_logic"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Instance of Category for propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Category Propositional Sign.Sign Morphism.Morphism where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- Identity morhpism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ide Propositional = Morphism.idMor
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- Returns the domain of a morphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder dom Propositional = Morphism.source
ebe517300051f765f2ed856a789dd5613d681ab0Klaus Luettich -- Returns the codomain of a morphism
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers cod Propositional = Morphism.target
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- all sets are legal objects
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder legal_obj Propositional s = Sign.isLegalSignature s
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- tests if the morphism is ok
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder legal_mor Propositional f = Morphism.isLegalMorphism f
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- composition of morphisms
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers comp Propositional f g = Morphism.composeMor f g
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Instance of Sentences for propositional logic
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance Sentences Propositional AS_BASIC.FORMULA Sign.ATP_ProofTree
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers Sign.Sign Morphism.Morphism Symbol.Symbol where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- returns the set of symbols
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers sym_of Propositional = Symbol.symOf
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- returns the symbol map
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers symmap_of Propositional = Symbol.getSymbolMap
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- returns the name of a symbol
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers sym_name Propositional = Symbol.getSymbolName
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- default entry
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers empty_proof_tree Propositional = error "Not yet implemented"
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- translation of sentences along signature morphism
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers map_sen Propositional = Morphism.mapSentence
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- there is nothing to leave out
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers simplify_sen Propositional _ form = form
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- supplied provers
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder#ifdef UNI_PACKAGE
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder provers Propositional = [Prove.zchaffProver]
0e012772df2ce0dc7e8f0fe3acf458c2871dcfbcChristian Maeder-- | Syntax of Propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Syntax Propositional AS_BASIC.BASIC_SPEC
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder AS_BASIC.SYMB_ITEMS AS_BASIC.SYMB_MAP_ITEMS where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder parse_basic_spec Propositional = Just Parse_AS.basicSpec
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder parse_symb_items _ = Nothing
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers parse_symb_map_items _ = Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Instance of Logic for propositional logc
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Logic Propositional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder stability Propositional = Experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder top_sublogic Propositional = Sublogic.top
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder all_sublogics Propositional = Sublogic.sublogics_all
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Static Analysis for propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance StaticAnalysis Propositional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder basic_analysis Propositional = Just $
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder empty_signature Propositional = Sign.emptySig
b391fd2c38849689e02c23dee372739eca29b7b6Christian Maeder inclusion Propositional = Morphism.inclusionMap
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich signature_union Propositional = Sign.sigUnion
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich is_subsig Propositional = Sign.isSubSigOf
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich signature_difference Propositional = Sign.diffOfSigs
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich sign_to_basic_spec Propositional = IAna.signToBasicSpec
19933e754a6a244efca3b63184fb191668e08931Klaus Luettich symbol_to_raw Propositional = Symbol.symbolToRaw
75cda7e5b890d050d560d970af244a183f28328fKlaus Luettich id_to_raw Propositional = Symbol.idToRaw
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich matches Propositional = Symbol.matches
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich stat_symb_items Propositional = Analysis.mkStatSymbItems
725a68ec81cba9b8aa8647bebfb5baa449803e7eKlaus Luettich stat_symb_map_items Propositional = Analysis.mkStatSymbMapItem
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich induced_from_morphism Propositional = Analysis.inducedFromMorphism
bf731ab5ef055c75bf26e8e5b2eb4a4a11ab61ebKlaus Luettich induced_from_to_morphism Propositional = Analysis.inducedFromToMorphism
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Sublogics
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance SemiLatticeWithTop Sublogic.PropSL where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL AS_BASIC.BASIC_SPEC where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic it = Sublogic.sl_basic_spec Sublogic.bottom it
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL Sign.Sign where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic si = Sublogic.sl_sig Sublogic.bottom si
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance Sublogics Sublogic.PropSL where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL AS_BASIC.FORMULA where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic frm = Sublogic.sl_form Sublogic.bottom frm
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL Symbol.Symbol where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic sym = Sublogic.sl_sym Sublogic.bottom sym
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL AS_BASIC.SYMB_ITEMS where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic symit = Sublogic.sl_symit Sublogic.bottom symit
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL Morphism.Morphism where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic symor = Sublogic.sl_mor Sublogic.bottom symor
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckersinstance MinSublogic Sublogic.PropSL AS_BASIC.SYMB_MAP_ITEMS where
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers minSublogic sm = Sublogic.sl_symmap Sublogic.bottom sm
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance ProjectSublogicM Sublogic.PropSL Symbol.Symbol where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder projectSublogicM = Sublogic.prSymbolM
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance ProjectSublogic Sublogic.PropSL Sign.Sign where
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder projectSublogic = Sublogic.prSig
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maederinstance ProjectSublogic Sublogic.PropSL Morphism.Morphism where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder projectSublogic = Sublogic.prMor
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maederinstance ProjectSublogicM Sublogic.PropSL AS_BASIC.SYMB_MAP_ITEMS where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder projectSublogicM = Sublogic.prSymMapM
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance ProjectSublogicM Sublogic.PropSL AS_BASIC.SYMB_ITEMS where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder projectSublogicM = Sublogic.prSymM
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maederinstance ProjectSublogic Sublogic.PropSL AS_BASIC.BASIC_SPEC where
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder projectSublogic = Sublogic.prBasicSpec
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maederinstance ProjectSublogicM Sublogic.PropSL AS_BASIC.FORMULA where
26f228bf3a3fea810223396e5794c217a79a8d5bChristian Maeder projectSublogicM = Sublogic.prFormulaM