hets/Propositional/Logic_Propositional.hs

	Logic_Propositional.hs revision a65c6747c9acbbebc93baba7bae94d2e3d8cdafb
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz{-# LANGUAGE CPP, MultiParamTypeClasses #-}
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzModule      :  $Header$
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzDescription :  Instance of class Logic for propositional logic
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright   :  (c) Dominik Luecke, Uni Bremen 2007
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzLicense     :  GPLv2 or higher, see LICENSE.txt
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzMaintainer  :  luecke@informatik.uni-bremen.de
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzStability   :  experimental
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzPortability :  non-portable (imports Logic.Logic)
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzInstance of class Logic for the propositional logic
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz   Also the instances for Syntax and Category.
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz-}
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz{-
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz  Ref.
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz  http://en.wikipedia.org/wiki/Propositional_logic
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz  What is a Logic?.
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz  2005.
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz-}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermodule Propositional.Logic_Propositional where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport ATC.ProofTree ()
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzimport Logic.Logic
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Sign
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Morphism
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.AS_BASIC_Propositional
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.ATC_Propositional ()
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzimport Propositional.Fold
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Symbol as Symbol
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzimport Propositional.Parse_AS_Basic
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Analysis
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Sublogic as Sublogic
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz#ifdef UNI_PACKAGE
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.ProveWithTruthTable
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Prove
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.Conservativity
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Propositional.ProveMinisat
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Common.ProverTools
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Common.Consistency
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder#endif
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport Common.ProofTree
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Id
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Monoid
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz-- | Lid for propositional logic
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzdata Propositional = Propositional deriving Show
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzinstance Language Propositional where
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz    description _ = "Propositional Logic\n"
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz        ++ "for more information please refer to\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder        ++ "http://en.wikipedia.org/wiki/Propositional_logic"
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz-- | Instance of Category for propositional logic
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulzinstance Category Sign Morphism where
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- Identity morhpism
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    ide = idMor
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- Returns the domain of a morphism
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    dom = source
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    -- Returns the codomain of a morphism
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    cod = target
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- check if morphism is inclusion
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    isInclusion = Map.null . propMap
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- tests if the morphism is ok
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    legal_mor = isLegalMorphism
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- composition of morphisms
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    composeMorphisms = composeMor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz-- | Instance of Sentences for propositional logic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Sentences Propositional FORMULA
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    Sign Morphism Symbol where
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    negation Propositional = Just . negForm nullRange
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- returns the set of symbols
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    sym_of Propositional = singletonList . symOf
2cba38ca53f268f204eb6916ebef0e9543a99e0aEwaryst Schulz    -- returns the symbol map
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    symmap_of Propositional = getSymbolMap
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz    -- returns the name of a symbol
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    sym_name Propositional = getSymbolName
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz    -- translation of sentences along signature morphism
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz    map_sen Propositional = mapSentence
    -- there is nothing to leave out
    simplify_sen Propositional _ = simplify

instance Monoid BASIC_SPEC where
    mempty = Basic_spec []
    mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

--- | Syntax of Propositional logic
instance Syntax Propositional BASIC_SPEC
    Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
         parsersAndPrinters Propositional =
           addSyntax "Hets" (basicSpec, pretty)
           $ makeDefault (basicSpec, pretty)
         parse_symb_items Propositional = Just symbItems
         parse_symb_map_items Propositional = Just symbMapItems

-- | Instance of Logic for propositional logc
instance Logic Propositional
    PropSL                    -- Sublogics
    BASIC_SPEC                -- basic_spec
    FORMULA                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
    ProofTree                      -- proof_tree
    where
      stability Propositional = Experimental
      top_sublogic Propositional = Sublogic.top
      all_sublogics Propositional = sublogics_all
      empty_proof_tree Propositional = emptyProofTree
    -- supplied provers
      provers Propositional = []
#ifdef UNI_PACKAGE
        ++ unsafeProverCheck "zchaff" "PATH" zchaffProver
        ++ unsafeProverCheck "minisat" "PATH" (minisatProver Minisat)
        ++ unsafeProverCheck "minisat2" "PATH" (minisatProver Minisat2)
        ++ [ttProver]
      cons_checkers Propositional = []
         ++ unsafeProverCheck "zchaff" "PATH" propConsChecker
         ++ unsafeProverCheck "minisat" "PATH" (minisatConsChecker Minisat)
         ++ unsafeProverCheck "minisat2" "PATH" (minisatConsChecker Minisat2)
         ++ [ttConsistencyChecker]
      conservativityCheck Propositional = []
          ++ unsafeProverCheck "sKizzo" "PATH"
             (ConservativityChecker "sKizzo" conserCheck)
          ++ [ConservativityChecker "Truth Tables" ttConservativityChecker]
#endif


-- | Static Analysis for propositional logic
instance StaticAnalysis Propositional
    BASIC_SPEC                -- basic_spec
    FORMULA                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
        where
          basic_analysis Propositional =
              Just basicPropositionalAnalysis
          empty_signature Propositional = emptySig
          is_subsig Propositional = isSubSigOf
          subsig_inclusion Propositional s = return . inclusionMap s
          signature_union Propositional = sigUnion
          symbol_to_raw Propositional = symbolToRaw
          id_to_raw Propositional = idToRaw
          matches Propositional = Symbol.matches
          stat_symb_items Propositional _ = mkStatSymbItems
          stat_symb_map_items Propositional _ _ = mkStatSymbMapItem
          morphism_union Propositional = morphismUnion
          induced_from_morphism Propositional = inducedFromMorphism
          induced_from_to_morphism Propositional = inducedFromToMorphism
          signature_colimit Propositional = signatureColimit

-- | Sublogics
instance SemiLatticeWithTop PropSL where
    join = sublogics_max
    top = Sublogic.top

instance MinSublogic PropSL BASIC_SPEC where
     minSublogic = sl_basic_spec bottom

instance MinSublogic PropSL Sign where
    minSublogic = sl_sig bottom

instance SublogicName PropSL where
    sublogicName = sublogics_name

instance MinSublogic PropSL FORMULA where
    minSublogic = sl_form bottom

instance MinSublogic PropSL Symbol where
    minSublogic = sl_sym bottom

instance MinSublogic PropSL SYMB_ITEMS where
    minSublogic = sl_symit bottom

instance MinSublogic PropSL Morphism where
    minSublogic = sl_mor bottom

instance MinSublogic PropSL SYMB_MAP_ITEMS where
    minSublogic = sl_symmap bottom

instance ProjectSublogicM PropSL Symbol where
    projectSublogicM = prSymbolM

instance ProjectSublogic PropSL Sign where
    projectSublogic = prSig

instance ProjectSublogic PropSL Morphism where
    projectSublogic = prMor

instance ProjectSublogicM PropSL SYMB_MAP_ITEMS where
    projectSublogicM = prSymMapM

instance ProjectSublogicM PropSL SYMB_ITEMS where
    projectSublogicM = prSymM

instance ProjectSublogic PropSL BASIC_SPEC where
    projectSublogic = prBasicSpec

instance ProjectSublogicM PropSL FORMULA where
    projectSublogicM = prFormulaM