```{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./Propositional/Logic_Propositional.hs
Description :  Instance of class Logic for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007

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.

http://en.wikipedia.org/wiki/Propositional_logic

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.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 ()

-- | Lid for propositional logic
data Propositional = Propositional deriving Int -> Propositional -> ShowS
[Propositional] -> ShowS
Propositional -> String
(Int -> Propositional -> ShowS)
-> (Propositional -> String)
-> ([Propositional] -> ShowS)
-> Show Propositional
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Propositional] -> ShowS
\$cshowList :: [Propositional] -> ShowS
show :: Propositional -> String
\$cshow :: Propositional -> String
showsPrec :: Int -> Propositional -> ShowS
\$cshowsPrec :: Int -> Propositional -> ShowS
Show

instance Language Propositional where
description :: Propositional -> String
description _ = "Propositional Logic\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "http://en.wikipedia.org/wiki/Propositional_logic"

-- | Instance of Category for propositional logic
instance Category Sign Morphism where
-- Identity morhpism
ide :: Sign -> Morphism
ide = Sign -> Morphism
idMor
-- Returns the domain of a morphism
dom :: Morphism -> Sign
dom = Morphism -> Sign
source
-- Returns the codomain of a morphism
cod :: Morphism -> Sign
cod = Morphism -> Sign
target
-- check if morphism is inclusion
isInclusion :: Morphism -> Bool
isInclusion = Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (Map Id Id -> Bool) -> (Morphism -> Map Id Id) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map Id Id
propMap
-- tests if the morphism is ok
legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
isLegalMorphism
-- composition of morphisms
composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
composeMor

-- | Instance of Sentences for propositional logic
instance Sentences Propositional FORMULA
Sign Morphism Symbol where
negation :: Propositional -> FORMULA -> Maybe FORMULA
negation Propositional = FORMULA -> Maybe FORMULA
forall a. a -> Maybe a
Just (FORMULA -> Maybe FORMULA)
-> (FORMULA -> FORMULA) -> FORMULA -> Maybe FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> FORMULA -> FORMULA
negForm Range
nullRange
-- returns the set of symbols
sym_of :: Propositional -> Sign -> [Set Symbol]
sym_of Propositional = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symOf
-- returns the symbol map
symmap_of :: Propositional -> Morphism -> EndoMap Symbol
symmap_of Propositional = Morphism -> EndoMap Symbol
getSymbolMap
-- returns the name of a symbol
sym_name :: Propositional -> Symbol -> Id
sym_name Propositional = Symbol -> Id
getSymbolName
symKind :: Propositional -> Symbol -> String
symKind Propositional _ = "prop"
-- translation of sentences along signature morphism
map_sen :: Propositional -> Morphism -> FORMULA -> Result FORMULA
map_sen Propositional = Morphism -> FORMULA -> Result FORMULA
mapSentence
-- there is nothing to leave out
simplify_sen :: Propositional -> Sign -> FORMULA -> FORMULA
simplify_sen Propositional _ = FORMULA -> FORMULA
simplify

instance Semigroup BASIC_SPEC where
(Basic_spec l1 :: [Annoted BASIC_ITEMS]
l1) <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> (Basic_spec l2 :: [Annoted BASIC_ITEMS]
l2) = [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEMS] -> BASIC_SPEC)
-> [Annoted BASIC_ITEMS] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
\$ [Annoted BASIC_ITEMS]
l1 [Annoted BASIC_ITEMS]
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEMS]
l2
instance Monoid BASIC_SPEC where
mempty :: BASIC_SPEC
mempty = [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec []

-- - | Syntax of Propositional logic
instance Syntax Propositional BASIC_SPEC
Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
parsersAndPrinters :: Propositional
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
parsersAndPrinters Propositional =
String
-> (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "Hets" (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
(Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc))
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall a b. (a -> b) -> a -> b
\$ (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. b -> Map String b
makeDefault (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
parse_symb_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Propositional = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
\$ AParser st SYMB_ITEMS
forall st. GenParser Char st SYMB_ITEMS
symbItems
parse_symb_map_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Propositional = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
-> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
\$ AParser st SYMB_MAP_ITEMS
forall st. GenParser Char st SYMB_MAP_ITEMS
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 -> Maybe (BASIC_SPEC -> AParser st FORMULA)
parse_basic_sen Propositional = (BASIC_SPEC -> AParser st FORMULA)
-> Maybe (BASIC_SPEC -> AParser st FORMULA)
forall a. a -> Maybe a
Just ((BASIC_SPEC -> AParser st FORMULA)
-> Maybe (BASIC_SPEC -> AParser st FORMULA))
-> (BASIC_SPEC -> AParser st FORMULA)
-> Maybe (BASIC_SPEC -> AParser st FORMULA)
forall a b. (a -> b) -> a -> b
\$ AParser st FORMULA -> BASIC_SPEC -> AParser st FORMULA
forall a b. a -> b -> a
const AParser st FORMULA
forall st. AParser st FORMULA
impFormula
stability :: Propositional -> Stability
stability Propositional = Stability
Stable
top_sublogic :: Propositional -> PropSL
top_sublogic Propositional = PropSL
Sublogic.top
all_sublogics :: Propositional -> [PropSL]
all_sublogics Propositional = [PropSL]
sublogics_all
empty_proof_tree :: Propositional -> ProofTree
empty_proof_tree Propositional = ProofTree
emptyProofTree
-- supplied provers
provers :: Propositional -> [Prover Sign FORMULA Morphism PropSL ProofTree]
provers Propositional =
[Prover Sign FORMULA Morphism PropSL ProofTree
zchaffProver, MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree
minisatProver MiniSatVer
Minisat, MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree
minisatProver MiniSatVer
Minisat2, Prover Sign FORMULA Morphism PropSL ProofTree
ttProver]
cons_checkers :: Propositional
-> [ConsChecker Sign FORMULA PropSL Morphism ProofTree]
cons_checkers Propositional =
[ ConsChecker Sign FORMULA PropSL Morphism ProofTree
propConsChecker, MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree
minisatConsChecker MiniSatVer
Minisat
, MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree
minisatConsChecker MiniSatVer
Minisat2, ConsChecker Sign FORMULA PropSL Morphism ProofTree
ttConsistencyChecker]
conservativityCheck :: Propositional -> [ConservativityChecker Sign FORMULA Morphism]
conservativityCheck Propositional =
[ String
-> IO (Maybe String)
-> ((Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA])))
-> ConservativityChecker Sign FORMULA Morphism
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
-> morphism
-> [Named sentence]
-> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker "sKizzo" (String -> IO (Maybe String)
checkBinary "sKizzo") (Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
conserCheck
, String
-> IO (Maybe String)
-> ((Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA])))
-> ConservativityChecker Sign FORMULA Morphism
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
-> morphism
-> [Named sentence]
-> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker "Truth Tables" (Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing)
(Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
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
-> Maybe
((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
basic_analysis Propositional =
((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe
((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
basicPropositionalAnalysis
sen_analysis :: Propositional
-> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
sen_analysis Propositional = ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
-> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, FORMULA) -> Result FORMULA
pROPsen_analysis
empty_signature :: Propositional -> Sign
empty_signature Propositional = Sign
emptySig
is_subsig :: Propositional -> Sign -> Sign -> Bool
is_subsig Propositional = Sign -> Sign -> Bool
isSubSigOf
subsig_inclusion :: Propositional -> Sign -> Sign -> Result Morphism
subsig_inclusion Propositional s :: Sign
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Sign -> Morphism) -> Sign -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Morphism
inclusionMap Sign
s
signature_union :: Propositional -> Sign -> Sign -> Result Sign
signature_union Propositional = Sign -> Sign -> Result Sign
sigUnion
symbol_to_raw :: Propositional -> Symbol -> Symbol
symbol_to_raw Propositional = Symbol -> Symbol
symbolToRaw
id_to_raw :: Propositional -> Id -> Symbol
id_to_raw Propositional = Id -> Symbol
idToRaw
matches :: Propositional -> Symbol -> Symbol -> Bool
matches Propositional = Symbol -> Symbol -> Bool
Symbol.matches
stat_symb_items :: Propositional -> Sign -> [SYMB_ITEMS] -> Result [Symbol]
stat_symb_items Propositional _ = [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems
stat_symb_map_items :: Propositional
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap Symbol)
stat_symb_map_items Propositional _ _ = [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol)
mkStatSymbMapItem
morphism_union :: Propositional -> Morphism -> Morphism -> Result Morphism
morphism_union Propositional = Morphism -> Morphism -> Result Morphism
morphismUnion
induced_from_morphism :: Propositional -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism Propositional = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
induced_from_to_morphism :: Propositional
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism Propositional = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
signature_colimit :: Propositional
-> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit Propositional = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit

-- | Sublogics
instance SemiLatticeWithTop PropSL where
lub :: PropSL -> PropSL -> PropSL
lub = PropSL -> PropSL -> PropSL
sublogics_max
top :: PropSL
top = PropSL
Sublogic.top

instance MinSublogic PropSL BASIC_SPEC where
minSublogic :: BASIC_SPEC -> PropSL
minSublogic = PropSL -> BASIC_SPEC -> PropSL
sl_basic_spec PropSL
bottom

instance MinSublogic PropSL Sign where
minSublogic :: Sign -> PropSL
minSublogic = PropSL -> Sign -> PropSL
sl_sig PropSL
bottom

instance SublogicName PropSL where
sublogicName :: PropSL -> String
sublogicName = PropSL -> String
sublogics_name

instance MinSublogic PropSL FORMULA where
minSublogic :: FORMULA -> PropSL
minSublogic = PropSL -> FORMULA -> PropSL
sl_form PropSL
bottom

instance MinSublogic PropSL Symbol where
minSublogic :: Symbol -> PropSL
minSublogic = PropSL -> Symbol -> PropSL
sl_sym PropSL
bottom

instance MinSublogic PropSL SYMB_ITEMS where
minSublogic :: SYMB_ITEMS -> PropSL
minSublogic = PropSL -> SYMB_ITEMS -> PropSL
sl_symit PropSL
bottom

instance MinSublogic PropSL Morphism where
minSublogic :: Morphism -> PropSL
minSublogic = PropSL -> Morphism -> PropSL
sl_mor PropSL
bottom

instance MinSublogic PropSL SYMB_MAP_ITEMS where
minSublogic :: SYMB_MAP_ITEMS -> PropSL
minSublogic = PropSL -> SYMB_MAP_ITEMS -> PropSL
sl_symmap PropSL
bottom

instance ProjectSublogicM PropSL Symbol where
projectSublogicM :: PropSL -> Symbol -> Maybe Symbol
projectSublogicM = PropSL -> Symbol -> Maybe Symbol
prSymbolM

instance ProjectSublogic PropSL Sign where
projectSublogic :: PropSL -> Sign -> Sign
projectSublogic = PropSL -> Sign -> Sign
prSig

instance ProjectSublogic PropSL Morphism where
projectSublogic :: PropSL -> Morphism -> Morphism
projectSublogic = PropSL -> Morphism -> Morphism
prMor

instance ProjectSublogicM PropSL SYMB_MAP_ITEMS where
projectSublogicM :: PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projectSublogicM = PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM

instance ProjectSublogicM PropSL SYMB_ITEMS where
projectSublogicM :: PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
projectSublogicM = PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymM

instance ProjectSublogic PropSL BASIC_SPEC where
projectSublogic :: PropSL -> BASIC_SPEC -> BASIC_SPEC
projectSublogic = PropSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec

instance ProjectSublogicM PropSL FORMULA where
projectSublogicM :: PropSL -> FORMULA -> Maybe FORMULA
projectSublogicM = PropSL -> FORMULA -> Maybe FORMULA
prFormulaM
```