Logic_QBF.hs revision e16b3696b2c173aac14200321868ed81b8f7dc69
cd47196ef7dd7647418fa9b9cb8297cfa614c100rbb{-# LANGUAGE MultiParamTypeClasses #-}
809c98e396829d27f2d9efc0c27f7bb1294381bcgsteinModule : $Header$
cd47196ef7dd7647418fa9b9cb8297cfa614c100rbbDescription : Instance of class Logic for propositional logic
cd47196ef7dd7647418fa9b9cb8297cfa614c100rbb extended with QBFs
306e22b1e932824368f6d9df002f72fb00e70ecdrjungCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
a93e781d9c03749f57328077b8350b09c40ce737sfLicense : GPLv2 or higher, see LICENSE.txt
4dee28b6fc8fff5efde4e7821aeb6defed3fb84dsfMaintainer : jonathan.von_schroeder@dfki.de
acc9093ae1f3c97acc635bd5b2c7c0969da21183trawickStability : experimental
306e22b1e932824368f6d9df002f72fb00e70ecdrjungPortability : non-portable (imports Logic.Logic)
7bffd59eadbb9e58f17fd29655fce6509fc1bb36niqInstance of class Logic for the propositional logic extended with QBFs
a93e781d9c03749f57328077b8350b09c40ce737sf Also the instances for Syntax and Category.
ef8dbafa2d1039dd720b6262069508377b1a9d13jorton Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
ef8dbafa2d1039dd720b6262069508377b1a9d13jorton What is a Logic?.
ef8dbafa2d1039dd720b6262069508377b1a9d13jorton In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjungimport QBF.Sublogic as Sublogic
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzimport QBF.Symbol as Symbol
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzimport qualified Data.Map as Map
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz-- | Lid for propositional logic
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzdata QBF = QBF deriving Show
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzinstance Language QBF where
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz description _ = "Propositional Logic extended with QBFs\n"
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz ++ "for more information please refer to\n"
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz ++ "http://en.wikipedia.org/wiki/Propositional_logic"
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz-- | Instance of Category for propositional logic
f29fb02bd92bbbb11b0231cc87d8b5d08875d821jortoninstance Category Sign Morphism where
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz -- Identity morhpism
53b3e9f9937ca992fb149d02d19223674c81c5a4rjung -- Returns the domain of a morphism
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz dom = source
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz -- Returns the codomain of a morphism
708fec3f1a67942d7ee00b8c57fb0aa4fb40dde2kbrand cod = target
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz -- check if morphism is inclusion
83966c75d36cc4daef61f66509ead1f019a29e2bwsanchez isInclusion = Map.null . propMap
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz -- tests if the morphism is ok
53b3e9f9937ca992fb149d02d19223674c81c5a4rjung legal_mor = isLegalMorphism
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz -- composition of morphisms
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz composeMorphisms = composeMor
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz-- | Instance of Sentences for propositional logic
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzinstance Sentences QBF FORMULA
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz Sign Morphism Symbol where
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz negation QBF = Just . negateFormula
f4c472b8dce3c2e559232dbb5b27ed2466922ea4jerenkrantz -- returns the set of symbols
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung sym_of QBF = singletonList . symOf
3bcb72c0b2797d2ec0b41bb9f4696e58be2c7043rjung -- returns the symbol map
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung symmap_of QBF = getSymbolMap
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung -- returns the name of a symbol
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung sym_name QBF = getSymbolName
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung -- translation of sentences along signature morphism
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung map_sen QBF = mapSentence
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung -- there is nothing to leave out
5b43275cebfb0ff9961ac462f3a96f7fe612d327rjung simplify_sen QBF _ = simplify
708fec3f1a67942d7ee00b8c57fb0aa4fb40dde2kbrandinstance Monoid BASICSPEC where
db3f27380cc3e42e61bf9c0598c8234f11117195rjung mempty = BasicSpec []
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz mappend (BasicSpec l1) (BasicSpec l2) = BasicSpec $ l1 ++ l2
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz-- | Syntax of Propositional logic
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantzinstance Syntax QBF BASICSPEC
ec1719a5748717f67dcd279bb64bd0da424ae450jerenkrantz SYMBITEMS SYMBMAPITEMS where
a1ac7d611ace926f78735a77d3f6058ed3ee5557niq parse_basic_spec QBF = Just basicSpec
a850b54017d9cf36fc8eb8065876feb925293428sf parse_symb_items QBF = Just symbItems
a850b54017d9cf36fc8eb8065876feb925293428sf parse_symb_map_items QBF = Just symbMapItems
a850b54017d9cf36fc8eb8065876feb925293428sf-- | Instance of Logic for propositional logc
a850b54017d9cf36fc8eb8065876feb925293428sfinstance Logic QBF
a850b54017d9cf36fc8eb8065876feb925293428sf QBFSL -- Sublogics
a850b54017d9cf36fc8eb8065876feb925293428sf BASICSPEC -- basic_spec
a850b54017d9cf36fc8eb8065876feb925293428sf FORMULA -- sentence
a850b54017d9cf36fc8eb8065876feb925293428sf SYMBITEMS -- symb_items
563aaa97b79122ca62d977d2576a1f780063e895rjung SYMBMAPITEMS -- symb_map_items
a850b54017d9cf36fc8eb8065876feb925293428sf Sign -- sign
a850b54017d9cf36fc8eb8065876feb925293428sf Morphism -- morphism
a850b54017d9cf36fc8eb8065876feb925293428sf Symbol -- symbol
a850b54017d9cf36fc8eb8065876feb925293428sf Symbol -- raw_symbol
a850b54017d9cf36fc8eb8065876feb925293428sf ProofTree -- proof_tree
a850b54017d9cf36fc8eb8065876feb925293428sf stability QBF = Experimental
a850b54017d9cf36fc8eb8065876feb925293428sf top_sublogic QBF = Sublogic.top
a850b54017d9cf36fc8eb8065876feb925293428sf all_sublogics QBF = sublogicsAll
a850b54017d9cf36fc8eb8065876feb925293428sf empty_proof_tree QBF = emptyProofTree
a850b54017d9cf36fc8eb8065876feb925293428sf -- supplied provers
a850b54017d9cf36fc8eb8065876feb925293428sf provers QBF = []
a850b54017d9cf36fc8eb8065876feb925293428sf ++ unsafeProverCheck "depqbf" "PATH" depQBFProver
a850b54017d9cf36fc8eb8065876feb925293428sf-- | Static Analysis for propositional logic
a850b54017d9cf36fc8eb8065876feb925293428sfinstance StaticAnalysis QBF
708fec3f1a67942d7ee00b8c57fb0aa4fb40dde2kbrand BASICSPEC -- basic_spec
242165716294f4720e62d4b34670ef5145269bd8sctemme FORMULA -- sentence
a1ac7d611ace926f78735a77d3f6058ed3ee5557niq SYMBITEMS -- symb_items
a850b54017d9cf36fc8eb8065876feb925293428sf SYMBMAPITEMS -- symb_map_items
a1ac7d611ace926f78735a77d3f6058ed3ee5557niq Sign -- sign
a1ac7d611ace926f78735a77d3f6058ed3ee5557niq Morphism -- morphism
a850b54017d9cf36fc8eb8065876feb925293428sf Symbol -- symbol
a850b54017d9cf36fc8eb8065876feb925293428sf Symbol -- raw_symbol
708fec3f1a67942d7ee00b8c57fb0aa4fb40dde2kbrand basic_analysis QBF =
242165716294f4720e62d4b34670ef5145269bd8sctemme Just basicPropositionalAnalysis
a850b54017d9cf36fc8eb8065876feb925293428sf empty_signature QBF = emptySig
a850b54017d9cf36fc8eb8065876feb925293428sf is_subsig QBF = isSubSigOf
a850b54017d9cf36fc8eb8065876feb925293428sf subsig_inclusion QBF s = return . inclusionMap s
a850b54017d9cf36fc8eb8065876feb925293428sf signature_union QBF = sigUnion
a850b54017d9cf36fc8eb8065876feb925293428sf symbol_to_raw QBF = symbolToRaw
a1ac7d611ace926f78735a77d3f6058ed3ee5557niq id_to_raw QBF = idToRaw
3a330c2331fc04f7d3f0ce7741bb52b5823f97e1wrowe matches QBF = Symbol.matches
3a330c2331fc04f7d3f0ce7741bb52b5823f97e1wrowe stat_symb_items QBF _ = mkStatSymbItems
cd47196ef7dd7647418fa9b9cb8297cfa614c100rbb stat_symb_map_items QBF _ _ = mkStatSymbMapItem
top = Sublogic.top