{-# LANGUAGE MultiParamTypeClasses #-}
module Propositional.Logic_Propositional where
import ATC.ProofTree ()
import Logic.Logic
import Propositional.Sign
import Propositional.Morphism
import Propositional.AS_BASIC_Propositional
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.ProveWithTruthTable
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 ()
data Propositional = Propositional deriving Show
instance Language Propositional where
description _ = "Propositional Logic\n"
++ "for more information please refer to\n"
++ "http://en.wikipedia.org/wiki/Propositional_logic"
instance Category Sign Morphism where
ide = idMor
dom = source
cod = target
isInclusion = Map.null . propMap
legal_mor = isLegalMorphism
composeMorphisms = composeMor
instance Sentences Propositional FORMULA
Sign Morphism Symbol where
negation Propositional = Just . negForm nullRange
sym_of Propositional = singletonList . symOf
symmap_of Propositional = getSymbolMap
sym_name Propositional = getSymbolName
symKind Propositional _ = "prop"
map_sen Propositional = mapSentence
simplify_sen Propositional _ = simplify
instance Semigroup BASIC_SPEC where
(Basic_spec l1) <> (Basic_spec l2) = Basic_spec $ l1 ++ l2
instance Monoid BASIC_SPEC where
mempty = Basic_spec []
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 Logic Propositional
PropSL
BASIC_SPEC
FORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
Sign
Morphism
Symbol
Symbol
ProofTree
where
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
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]
instance StaticAnalysis Propositional
BASIC_SPEC
FORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
Sign
Morphism
Symbol
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
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