{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module : ./Propositional/Logic_Propositional.hs
Description : Instance of class Logic for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : experimental
Portability : non-portable (imports Logic.Logic)
Instance of class Logic for the propositional logic
Also the instances for Syntax and Category.
-}
{-
Ref.
Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
What is a Logic?.
In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
2005.
-}
module Propositional.Logic_Propositional where
import ATC.ProofTree ()
import Logic.Logic
import Propositional.Sign
import Propositional.Morphism
import Propositional.ATC_Propositional ()
import Propositional.Fold
import Propositional.Symbol as Symbol
import Propositional.Parse_AS_Basic
import Propositional.Analysis
import Propositional.Sublogic as Sublogic
import Propositional.Prove
import Propositional.Conservativity
import Propositional.ProveMinisat
import Common.ProverTools
import Common.Consistency
import Common.ProofTree
import Common.Id
import qualified Data.Map as Map
import Data.Monoid
-- | Lid for propositional logic
data Propositional = Propositional deriving Show
instance Language Propositional where
description _ = "Propositional Logic\n"
++ "for more information please refer to\n"
-- | Instance of Category for propositional logic
instance Category Sign Morphism where
-- Identity morhpism
ide = idMor
-- Returns the domain of a morphism
dom = source
-- Returns the codomain of a morphism
cod = target
-- check if morphism is inclusion
isInclusion = Map.null . propMap
-- tests if the morphism is ok
legal_mor = isLegalMorphism
-- composition of morphisms
composeMorphisms = composeMor
-- | Instance of Sentences for propositional logic
instance Sentences Propositional FORMULA
Sign Morphism Symbol where
negation Propositional = Just . negForm nullRange
-- returns the set of symbols
sym_of Propositional = singletonList . symOf
-- returns the symbol map
symmap_of Propositional = getSymbolMap
-- returns the name of a symbol
sym_name Propositional = getSymbolName
symKind Propositional _ = "prop"
-- translation of sentences along signature morphism
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
-- hybridization
parse_basic_sen Propositional = Just $ const impFormula
stability Propositional = Stable
top_sublogic Propositional = Sublogic.top
all_sublogics Propositional = sublogics_all
empty_proof_tree Propositional = emptyProofTree
-- supplied provers
provers Propositional =
[zchaffProver, minisatProver Minisat, minisatProver Minisat2, ttProver]
cons_checkers Propositional =
[ propConsChecker, minisatConsChecker Minisat
, minisatConsChecker Minisat2, ttConsistencyChecker]
conservativityCheck Propositional =
[ ConservativityChecker "sKizzo" (checkBinary "sKizzo") conserCheck
, ConservativityChecker "Truth Tables" (return Nothing)
ttConservativityChecker]
-- | 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
sen_analysis Propositional = Just pROPsen_analysis
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
lub = 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