8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses #-}
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederDescription : Instance of class Logic for propositional logic
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder extended with QBFs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
6820f0de92751e29d73d64db48e776591f529a76Christian MaederMaintainer : jonathan.von_schroeder@dfki.de
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederStability : experimental
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederPortability : non-portable (imports Logic.Logic)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederInstance of class Logic for the propositional logic extended with QBFs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Also the instances for Syntax and Category.
6820f0de92751e29d73d64db48e776591f529a76Christian Maeder <http://en.wikipedia.org/wiki/Propositional_logic>
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder What is a Logic?.
6820f0de92751e29d73d64db48e776591f529a76Christian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport QBF.Sublogic as Sublogic
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport QBF.Symbol as Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Map as Map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Lid for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederdata QBF = QBF deriving Show
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Language QBF where
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski description _ = "Propositional Logic extended with quantified boolean formulas\n"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ "for more information please refer to\n"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ "http://en.wikipedia.org/wiki/Propositional_logic"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ++ "http://www.voronkov.com/lics.cgi"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Instance of Category for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Category Sign Morphism where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- Identity morhpism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- Returns the domain of a morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- Returns the codomain of a morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- check if morphism is inclusion
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder isInclusion = Map.null . propMap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- tests if the morphism is ok
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder legal_mor = isLegalMorphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- composition of morphisms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder composeMorphisms = composeMor
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Instance of Sentences for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Sentences QBF FORMULA
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Sign Morphism Symbol where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder negation QBF = Just . negateFormula
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- returns the set of symbols
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sym_of QBF = singletonList . symOf
dce9807ffe25e6ee055869248bcb85ba9dcaa026mscodescu -- kind of symbols is always prop
dce9807ffe25e6ee055869248bcb85ba9dcaa026mscodescu symKind QBF _ = "prop"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- returns the symbol map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder symmap_of QBF = getSymbolMap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- returns the name of a symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sym_name QBF = getSymbolName
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- translation of sentences along signature morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder map_sen QBF = mapSentence
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- there is nothing to leave out
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder simplify_sen QBF _ = simplify
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederinstance Monoid BASICSPEC where
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mempty = BasicSpec []
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mappend (BasicSpec l1) (BasicSpec l2) = BasicSpec $ l1 ++ l2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Syntax of Propositional logic
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Syntax QBF BASICSPEC Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder SYMBITEMS SYMBMAPITEMS where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_basic_spec QBF = Just basicSpec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_symb_items QBF = Just symbItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder parse_symb_map_items QBF = Just symbMapItems
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Instance of Logic for propositional logc
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Logic QBF
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroeder QBFSL -- Sublogics
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder BASICSPEC -- basic_spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder FORMULA -- sentence
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder SYMBITEMS -- symb_items
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder SYMBMAPITEMS -- symb_map_items
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism -- morphism
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroeder Symbol -- symbol
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroeder Symbol -- raw_symbol
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroeder ProofTree -- proof_tree
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability QBF = Stable
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder top_sublogic QBF = Sublogic.top
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder all_sublogics QBF = sublogicsAll
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder empty_proof_tree QBF = emptyProofTree
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -- supplied provers
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder provers QBF = [depQBFProver]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Static Analysis for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance StaticAnalysis QBF
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder BASICSPEC -- basic_spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder FORMULA -- sentence
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder SYMBITEMS -- symb_items
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder SYMBMAPITEMS -- symb_map_items
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism -- morphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Symbol -- symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Symbol -- raw_symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder basic_analysis QBF =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Just basicPropositionalAnalysis
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder empty_signature QBF = emptySig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder is_subsig QBF = isSubSigOf
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder subsig_inclusion QBF s = return . inclusionMap s
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder signature_union QBF = sigUnion
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder symbol_to_raw QBF = symbolToRaw
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder id_to_raw QBF = idToRaw
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder stat_symb_items QBF _ = mkStatSymbItems
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder stat_symb_map_items QBF _ _ = mkStatSymbMapItem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder morphism_union QBF = morphismUnion
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder induced_from_morphism QBF = inducedFromMorphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder induced_from_to_morphism QBF = inducedFromToMorphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder signature_colimit QBF = signatureColimit
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance SemiLatticeWithTop QBFSL where
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder lub = sublogicsMax
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL BASICSPEC where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slBasicSpec bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL Sign where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slSig bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance SublogicName QBFSL where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder sublogicName = sublogicsName
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL FORMULA where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slForm bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL Symbol where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slSym bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL SYMBITEMS where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slSymit bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL Morphism where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slMor bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance MinSublogic QBFSL SYMBMAPITEMS where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder minSublogic = slSymmap bottom
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogicM QBFSL Symbol where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogicM = prSymbolM
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogic QBFSL Sign where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogic = prSig
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogic QBFSL Morphism where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogic = prMor
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogicM QBFSL SYMBMAPITEMS where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogicM = prSymMapM
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogicM QBFSL SYMBITEMS where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogicM = prSymM
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogic QBFSL BASICSPEC where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogic = prBasicSpec
d71447e45047d07006b4c20409fbd8ea287df01fJonathan von Schroederinstance ProjectSublogicM QBFSL FORMULA where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder projectSublogicM = prFormulaM