Logic_QBF.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb{-# LANGUAGE MultiParamTypeClasses #-}
33bdcae1f7a1a65e351dda2a766a0cf28b1e695dndDescription : Instance of class Logic for propositional logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb extended with QBFs
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbLicense : GPLv2 or higher, see LICENSE.txt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : jonathan.von_schroeder@dfki.de
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStability : experimental
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : non-portable (imports Logic.Logic)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbInstance of class Logic for the propositional logic extended with QBFs
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Also the instances for Syntax and Category.
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb What is a Logic?.
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport QBF.Sublogic as Sublogic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport QBF.Symbol as Symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified Data.Map as Map
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | Lid for propositional logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbdata QBF = QBF deriving Show
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Language QBF where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb description _ = "Propositional Logic extended with QBFs\n"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ++ "for more information please refer to\n"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | Instance of Category for propositional logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Category Sign Morphism where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- Identity morhpism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ide = idMor
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- Returns the domain of a morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb dom = source
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- Returns the codomain of a morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb cod = target
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- check if morphism is inclusion
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb isInclusion = Map.null . propMap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- tests if the morphism is ok
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb legal_mor = isLegalMorphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- composition of morphisms
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb composeMorphisms = composeMor
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | Instance of Sentences for propositional logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Sentences QBF FORMULA
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Sign Morphism Symbol where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb negation QBF = Just . negateFormula
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- returns the set of symbols
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sym_of QBF = singletonList . symOf
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- returns the symbol map
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb symmap_of QBF = getSymbolMap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- returns the name of a symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sym_name QBF = getSymbolName
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- translation of sentences along signature morphism
f888346b48f5e5b5e3f0a47dedb8cefd2759a4e2gregames map_sen QBF = mapSentence
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- there is nothing to leave out
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb simplify_sen QBF _ = simplify
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Monoid BASICSPEC where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb mempty = BasicSpec []
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb mappend (BasicSpec l1) (BasicSpec l2) = BasicSpec $ l1 ++ l2
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | Syntax of Propositional logic
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzinstance Syntax QBF BASICSPEC Symbol
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz SYMBITEMS SYMBMAPITEMS where
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz parse_basic_spec QBF = Just basicSpec
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz parse_symb_items QBF = Just symbItems
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz parse_symb_map_items QBF = Just symbMapItems
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- | Instance of Logic for propositional logc
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzinstance Logic QBF
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz QBFSL -- Sublogics
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb BASICSPEC -- basic_spec
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb FORMULA -- sentence
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb SYMBITEMS -- symb_items
4f9c22c4f27571d54197be9674e1fc0d528192aestriker SYMBMAPITEMS -- symb_map_items
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwrowe Sign -- sign
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Morphism -- morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Symbol -- symbol
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Symbol -- raw_symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ProofTree -- proof_tree
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb stability QBF = Experimental
4f9c22c4f27571d54197be9674e1fc0d528192aestriker top_sublogic QBF = Sublogic.top
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb all_sublogics QBF = sublogicsAll
4f9c22c4f27571d54197be9674e1fc0d528192aestriker empty_proof_tree QBF = emptyProofTree
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- supplied provers
4f9c22c4f27571d54197be9674e1fc0d528192aestriker provers QBF = [depQBFProver]
4f9c22c4f27571d54197be9674e1fc0d528192aestriker-- | Static Analysis for propositional logic
4f9c22c4f27571d54197be9674e1fc0d528192aestrikerinstance StaticAnalysis QBF
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb BASICSPEC -- basic_spec
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe FORMULA -- sentence
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe SYMBITEMS -- symb_items
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe SYMBMAPITEMS -- symb_map_items
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Sign -- sign
2d399cd7535887fceaa9f8f116eb98ce68ddd602trawick Morphism -- morphism
c2cf53a40a9814eb91db2cdf820f97d943f21628coar Symbol -- symbol
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Symbol -- raw_symbol
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar basic_analysis QBF =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Just basicPropositionalAnalysis
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar empty_signature QBF = emptySig
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe is_subsig QBF = isSubSigOf
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe subsig_inclusion QBF s = return . inclusionMap s
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe signature_union QBF = sigUnion
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe symbol_to_raw QBF = symbolToRaw
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe id_to_raw QBF = idToRaw
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe matches QBF = Symbol.matches
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe stat_symb_items QBF _ = mkStatSymbItems
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe stat_symb_map_items QBF _ _ = mkStatSymbMapItem
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe morphism_union QBF = morphismUnion
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames induced_from_morphism QBF = inducedFromMorphism
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe induced_from_to_morphism QBF = inducedFromToMorphism
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe signature_colimit QBF = signatureColimit
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe-- | Sublogics
8419e6f8bff1a3617933f3ba760d2bdec7442f44coarinstance SemiLatticeWithTop QBFSL where
8419e6f8bff1a3617933f3ba760d2bdec7442f44coar lub = sublogicsMax
8419e6f8bff1a3617933f3ba760d2bdec7442f44coarinstance MinSublogic QBFSL BASICSPEC where
8419e6f8bff1a3617933f3ba760d2bdec7442f44coar minSublogic = slBasicSpec bottom
8419e6f8bff1a3617933f3ba760d2bdec7442f44coarinstance MinSublogic QBFSL Sign where
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz minSublogic = slSig bottom
8419e6f8bff1a3617933f3ba760d2bdec7442f44coarinstance SublogicName QBFSL where
8419e6f8bff1a3617933f3ba760d2bdec7442f44coar sublogicName = sublogicsName
8419e6f8bff1a3617933f3ba760d2bdec7442f44coarinstance MinSublogic QBFSL FORMULA where
8419e6f8bff1a3617933f3ba760d2bdec7442f44coar minSublogic = slForm bottom
2a6e98ba4ffa30ded5d8831664c5cb2a170a56b6coarinstance MinSublogic QBFSL Symbol where
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz minSublogic = slSym bottom
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinstance MinSublogic QBFSL SYMBITEMS where
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe minSublogic = slSymit bottom
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinstance MinSublogic QBFSL Morphism where
4f9c22c4f27571d54197be9674e1fc0d528192aestriker minSublogic = slMor bottom
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregamesinstance MinSublogic QBFSL SYMBMAPITEMS where
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe minSublogic = slSymmap bottom
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweinstance ProjectSublogicM QBFSL Symbol where
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe projectSublogicM = prSymbolM
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinstance ProjectSublogic QBFSL Sign where
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe projectSublogic = prSig
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweinstance ProjectSublogic QBFSL Morphism where
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe projectSublogic = prMor
4f9c22c4f27571d54197be9674e1fc0d528192aestrikerinstance ProjectSublogicM QBFSL SYMBMAPITEMS where
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe projectSublogicM = prSymMapM
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweinstance ProjectSublogicM QBFSL SYMBITEMS where
c2cf53a40a9814eb91db2cdf820f97d943f21628coar projectSublogicM = prSymM
4775dfc34c90fada8c7c4d6a57ed8a3114d55c2dtrawickinstance ProjectSublogic QBFSL BASICSPEC where
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe projectSublogic = prBasicSpec
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweinstance ProjectSublogicM QBFSL FORMULA where
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe projectSublogicM = prFormulaM