Logic_QBF.hs revision a65c6747c9acbbebc93baba7bae94d2e3d8cdafb
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu{-# LANGUAGE MultiParamTypeClasses #-}
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuModule : $Header$
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederDescription : Instance of class Logic for propositional logic
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu extended with QBFs
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuMaintainer : jonathan.von_schroeder@dfki.de
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuStability : experimental
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuPortability : non-portable (imports Logic.Logic)
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela TurcuInstance of class Logic for the propositional logic extended with QBFs
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu Also the instances for Syntax and Category.
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu <http://en.wikipedia.org/wiki/Propositional_logic>
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder What is a Logic?.
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuimport QBF.Sublogic as Sublogic
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuimport QBF.Symbol as Symbol
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuimport qualified Data.Map as Map
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu-- | Lid for propositional logic
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcudata QBF = QBF deriving Show
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuinstance Language QBF where
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder description _ = "Propositional Logic extended with QBFs\n"
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder ++ "for more information please refer to\n"
3f5d611a1388ce3cd33f86da3f1e9b7ad68d087cMihaela Turcu ++ "http://en.wikipedia.org/wiki/Propositional_logic"
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu-- | Instance of Category for propositional logic
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcuinstance Category Sign Morphism where
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu -- Identity morhpism
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu -- Returns the domain of a morphism
d20b265a2765e843986ceed6bf0055582981bf0fChristian Maeder -- Returns the codomain of a morphism
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder -- check if morphism is inclusion
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder isInclusion = Map.null . propMap
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder -- tests if the morphism is ok
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder legal_mor = isLegalMorphism
1070181294f9381ac4ac19eba1c3ecc40fc731a4Mihaela Turcu -- composition of morphisms
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder composeMorphisms = composeMor
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder-- | Instance of Sentences for propositional logic
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maederinstance Sentences QBF FORMULA
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder Sign Morphism Symbol where
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder negation QBF = Just . negateFormula
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder -- returns the set of symbols
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder sym_of QBF = singletonList . symOf
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder -- returns the symbol map
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder symmap_of QBF = getSymbolMap
d20b265a2765e843986ceed6bf0055582981bf0fChristian Maeder -- returns the name of a symbol
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder sym_name QBF = getSymbolName
64610ae60115fa0465d6d8548827b13d214cdc9eChristian Maeder -- translation of sentences along signature morphism
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder map_sen QBF = mapSentence
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder -- there is nothing to leave out
17f1de180b775332d98ff24c7ce51d6866272dcdChristian Maeder simplify_sen QBF _ = simplify
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maederinstance Monoid BASICSPEC where
de2d031e186086e2cb775bc59bacda87c9b18371Christian Maeder mempty = BasicSpec []
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder mappend (BasicSpec l1) (BasicSpec l2) = BasicSpec $ l1 ++ l2
7cfd47f6dc4147e9a3d21d72f68c6325552092f0Christian Maeder-- | Syntax of Propositional logic
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maederinstance Syntax QBF BASICSPEC Symbol
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder SYMBITEMS SYMBMAPITEMS where
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder parse_basic_spec QBF = Just basicSpec
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder parse_symb_items QBF = Just symbItems
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder parse_symb_map_items QBF = Just symbMapItems
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder-- | Instance of Logic for propositional logc
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maederinstance Logic QBF
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder QBFSL -- Sublogics
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder BASICSPEC -- basic_spec
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder FORMULA -- sentence
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder SYMBITEMS -- symb_items
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder SYMBMAPITEMS -- symb_map_items
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder Morphism -- morphism
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Symbol -- symbol
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Symbol -- raw_symbol
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder ProofTree -- proof_tree
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder stability QBF = Experimental
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder top_sublogic QBF = Sublogic.top
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder all_sublogics QBF = sublogicsAll
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder empty_proof_tree QBF = emptyProofTree
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder -- supplied provers
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder provers QBF = []
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder ++ unsafeProverCheck "depqbf" "PATH" depQBFProver
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder-- | Static Analysis for propositional logic
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maederinstance StaticAnalysis QBF
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder BASICSPEC -- basic_spec
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder FORMULA -- sentence
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder SYMBITEMS -- symb_items
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder SYMBMAPITEMS -- symb_map_items
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Morphism -- morphism
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Symbol -- symbol
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Symbol -- raw_symbol
53d2d31717e8c65bb3c2d1f2cd891d626cf45e5bChristian Maeder basic_analysis QBF =
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder Just basicPropositionalAnalysis
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder empty_signature QBF = emptySig
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder is_subsig QBF = isSubSigOf
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder subsig_inclusion QBF s = return . inclusionMap s
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder signature_union QBF = sigUnion
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder symbol_to_raw QBF = symbolToRaw
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder id_to_raw QBF = idToRaw
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder stat_symb_items QBF _ = mkStatSymbItems
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder stat_symb_map_items QBF _ _ = mkStatSymbMapItem
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder morphism_union QBF = morphismUnion
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder induced_from_morphism QBF = inducedFromMorphism
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder induced_from_to_morphism QBF = inducedFromToMorphism
712ff727df7fe324064a1082a40d66a18a3df352Christian Maeder signature_colimit QBF = signatureColimit
dc792317de0a95aac4e9a6dadfb78df050e5022eChristian Maeder-- | Sublogics
top = Sublogic.top