{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./QBF/Sublogic.hs
Description : Sublogics for propositional logic
Copyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : <jonathan.von_schroeder@dfki.de>
Stability : experimental
Portability : non-portable (imports Logic.Logic)
Sublogics for Propositional Logic
-}
{-
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 QBF.Sublogic
(
slBasicSpec -- determine sublogic for basic spec
, QBFFormulae (..) -- types of propositional formulae
, QBFSL (..) -- sublogics for propositional logic
, sublogicsMax -- join of sublogics
, top -- Propositional
, bottom -- Horn
, sublogicsAll -- all sublogics
, sublogicsName -- name of sublogics
, slSig -- sublogic for a signature
, slForm -- sublogic for a formula
, slSym -- sublogic for symbols
, slSymit -- sublogic for symbol items
, slMor -- sublogic for morphisms
, slSymmap -- sublogic for symbol map items
, prSymbolM -- projection of symbols
, prSig -- projections of signatures
, prMor -- projections of morphisms
, prSymMapM -- projections of symbol maps
, prSymM -- projections of SYMBITEMS
, prFormulaM -- projections of formulae
, prBasicSpec -- projections of basic specs
, isProp
, isHC
)
where
import qualified QBF.Tools as Tools
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Symbol as Symbol
import qualified QBF.Morphism as Morphism
import qualified Propositional.Sign as Sign
import qualified Common.Lib.State as State
import qualified Common.AS_Annotation as AS_Anno
import Data.Data
-- | types of propositional formulae
data QBFFormulae = PlainFormula -- Formula without structural constraints
| HornClause -- Horn Clause Formulae
deriving (Show, Eq, Ord, Typeable, Data)
-- | sublogics for propositional logic
data QBFSL = QBFSL
{
format :: QBFFormulae -- Structural restrictions
} deriving (Show, Eq, Ord, Typeable, Data)
isProp :: QBFSL -> Bool
isProp sl = format sl == PlainFormula
isHC :: QBFSL -> Bool
isHC sl = format sl == HornClause
-- | comparison of sublogics
compareLE :: QBFSL -> QBFSL -> Bool
compareLE p1 p2 =
let f1 = format p1
f2 = format p2
in
case (f1, f2) of
(_, PlainFormula) -> True
(HornClause, HornClause) -> True
(_, HornClause) -> False
-- Special elements in the Lattice of logics
top :: QBFSL
top = QBFSL PlainFormula
bottom :: QBFSL
bottom = QBFSL HornClause
needPF :: QBFSL
needPF = bottom { format = PlainFormula }
-- join and max
sublogicsJoin :: (QBFFormulae -> QBFFormulae -> QBFFormulae)
-> QBFSL -> QBFSL -> QBFSL
sublogicsJoin pfF a b = QBFSL
{
format = pfF (format a) (format b)
}
joinType :: QBFFormulae -> QBFFormulae -> QBFFormulae
joinType HornClause HornClause = HornClause
joinType _ _ = PlainFormula
sublogicsMax :: QBFSL -> QBFSL -> QBFSL
sublogicsMax = sublogicsJoin joinType
-- Helpers
-- compute sublogics from a list of sublogics
compList :: [QBFSL] -> QBFSL
compList = foldl sublogicsMax bottom
{- Functions to compute minimal sublogic for a given element, these work
by recursing into all subelements -}
-- | determines the sublogic for symbol map items
slSymmap :: QBFSL -> AS_BASIC.SYMBMAPITEMS -> QBFSL
slSymmap ps _ = ps
-- | determines the sublogic for a morphism
slMor :: QBFSL -> Morphism.Morphism -> QBFSL
slMor ps _ = ps
-- | determines the sublogic for a Signature
slSig :: QBFSL -> Sign.Sign -> QBFSL
slSig ps _ = ps
-- | determines the sublogic for Symbol items
slSymit :: QBFSL -> AS_BASIC.SYMBITEMS -> QBFSL
slSymit ps _ = ps
-- | determines the sublogic for symbols
slSym :: QBFSL -> Symbol.Symbol -> QBFSL
slSym ps _ = ps
-- | determines sublogic for formula
slForm :: QBFSL -> AS_BASIC.FORMULA -> QBFSL
slForm ps = slFlForm ps . Tools.flatten
-- | determines sublogic for flattened formula
slFlForm :: QBFSL -> [AS_BASIC.FORMULA] -> QBFSL
slFlForm ps = foldl sublogicsMax ps
. map (\ x -> State.evalState (anaForm ps x) 0)
-- analysis of single "clauses"
anaForm :: QBFSL -> AS_BASIC.FORMULA -> State.State Int QBFSL
anaForm ps f =
case f of
AS_BASIC.Conjunction l _ ->
do
st <- State.get
return $ sublogicsMax needPF $ compList $ map
(\ x -> State.evalState (anaForm ps x) (st + 1)) l
AS_BASIC.Implication l m _ ->
do
st <- State.get
let analyze = sublogicsMax needPF $ sublogicsMax
((\ x -> State.evalState (anaForm ps x) (st + 1)) l)
((\ x -> State.evalState (anaForm ps x) (st + 1)) m)
return $
if st < 1 && format ps == HornClause && checkHornPos l m
then
ps
else
analyze
AS_BASIC.Equivalence l m _ ->
do
st <- State.get
return $ sublogicsMax needPF $ sublogicsMax
((\ x -> State.evalState (anaForm ps x) (st + 1)) l)
((\ x -> State.evalState (anaForm ps x) (st + 1)) m)
AS_BASIC.Negation l _ ->
if isLiteral l
then
return ps
else
do
st <- State.get
return $ (\ x -> State.evalState (anaForm ps x) (st + 1)) l
AS_BASIC.Disjunction l _ ->
let lprime = concatMap Tools.flattenDis l in
if all isLiteral lprime
then return $
if moreThanNLit lprime 1
then sublogicsMax needPF ps
else ps
else
do
st <- State.get
return $ sublogicsMax needPF $ compList $ map
(\ x -> State.evalState (anaForm ps x) (st + 1))
lprime
AS_BASIC.TrueAtom _ -> return ps
AS_BASIC.FalseAtom _ -> return ps
AS_BASIC.Predication _ -> return ps
AS_BASIC.ForAll {} -> return needPF
AS_BASIC.Exists {} -> return needPF
moreThanNLit :: [AS_BASIC.FORMULA] -> Int -> Bool
moreThanNLit = (>) . foldl (\ y x -> if x then y + 1 else y) 0
. map isPosLiteral
-- determines wheter a Formula is a literal
isLiteral :: AS_BASIC.FORMULA -> Bool
isLiteral (AS_BASIC.Predication _) = True
isLiteral (AS_BASIC.Negation (AS_BASIC.Predication _) _ ) = True
isLiteral (AS_BASIC.Negation _ _) = False
isLiteral (AS_BASIC.Conjunction _ _) = False
isLiteral (AS_BASIC.Implication {}) = False
isLiteral (AS_BASIC.Equivalence {}) = False
isLiteral (AS_BASIC.Disjunction _ _) = False
isLiteral (AS_BASIC.ForAll {}) = False
isLiteral (AS_BASIC.Exists {}) = False
isLiteral (AS_BASIC.TrueAtom _) = True
isLiteral (AS_BASIC.FalseAtom _) = True
-- determines wheter a Formula is a positive literal
isPosLiteral :: AS_BASIC.FORMULA -> Bool
isPosLiteral (AS_BASIC.Predication _) = True
isPosLiteral (AS_BASIC.Negation _ _) = False
isPosLiteral (AS_BASIC.Conjunction _ _) = False
isPosLiteral (AS_BASIC.Implication {}) = False
isPosLiteral (AS_BASIC.Equivalence {}) = False
isPosLiteral (AS_BASIC.Disjunction _ _) = False
isPosLiteral (AS_BASIC.ForAll {}) = False
isPosLiteral (AS_BASIC.Exists {}) = False
isPosLiteral (AS_BASIC.TrueAtom _ ) = True
isPosLiteral (AS_BASIC.FalseAtom _) = True
-- | determines subloig for basic items
slBasicItems :: QBFSL -> AS_BASIC.BASICITEMS -> QBFSL
slBasicItems ps bi =
case bi of
AS_BASIC.PredDecl _ -> ps
AS_BASIC.AxiomItems xs -> compList $ map (slForm ps . AS_Anno.item) xs
-- | determines sublogic for basic spec
slBasicSpec :: QBFSL -> AS_BASIC.BASICSPEC -> QBFSL
slBasicSpec ps (AS_BASIC.BasicSpec spec) =
compList $ map (slBasicItems ps . AS_Anno.item) spec
-- | all sublogics
sublogicsAll :: [QBFSL]
sublogicsAll =
[QBFSL
{
format = HornClause
}
, QBFSL
{
format = PlainFormula
}
]
-- Conversion functions to String
sublogicsName :: QBFSL -> String
sublogicsName f = case format f of
HornClause -> "HornClause"
PlainFormula -> "Prop"
-- Projections to sublogics
prSymbolM :: QBFSL -> Symbol.Symbol -> Maybe Symbol.Symbol
prSymbolM _ = Just
prSig _ sig = sig
prMor :: QBFSL -> Morphism.Morphism -> Morphism.Morphism
prMor _ mor = mor
prSymMapM :: QBFSL
-> Maybe AS_BASIC.SYMBMAPITEMS
prSymMapM _ = Just
prSymM :: QBFSL -> AS_BASIC.SYMBITEMS -> Maybe AS_BASIC.SYMBITEMS
prSymM _ = Just
-- keep an element if its computed sublogic is in the given sublogic
prFormulaM :: QBFSL -> AS_BASIC.FORMULA -> Maybe AS_BASIC.FORMULA
prFormulaM sl form
| compareLE (slForm bottom form) sl = Just form
| otherwise = Nothing
prPredItem :: QBFSL -> AS_BASIC.PREDITEM -> AS_BASIC.PREDITEM
prPredItem _ prI = prI
prBASICItems :: QBFSL -> AS_BASIC.BASICITEMS -> AS_BASIC.BASICITEMS
prBASICItems pSL bI =
case bI of
AS_BASIC.PredDecl pI -> AS_BASIC.PredDecl $ prPredItem pSL pI
AS_BASIC.AxiomItems aIS -> AS_BASIC.AxiomItems $ concatMap mapH aIS
where
mapH :: AS_Anno.Annoted AS_BASIC.FORMULA
mapH annoForm = let formP = prFormulaM pSL $ AS_Anno.item annoForm in
case formP of
Nothing -> []
Just f -> [ AS_Anno.Annoted
{
AS_Anno.item = f
, AS_Anno.opt_pos = AS_Anno.opt_pos annoForm
, AS_Anno.l_annos = AS_Anno.l_annos annoForm
, AS_Anno.r_annos = AS_Anno.r_annos annoForm
}
]
prBasicSpec :: QBFSL -> AS_BASIC.BASICSPEC -> AS_BASIC.BASICSPEC
prBasicSpec pSL (AS_BASIC.BasicSpec bS) =
AS_BASIC.BasicSpec $ map mapH bS
where
mapH :: AS_Anno.Annoted AS_BASIC.BASICITEMS
mapH aBI = AS_Anno.Annoted
{
AS_Anno.item = prBASICItems pSL $ AS_Anno.item aBI
, AS_Anno.opt_pos = AS_Anno.opt_pos aBI
, AS_Anno.l_annos = AS_Anno.l_annos aBI
, AS_Anno.r_annos = AS_Anno.r_annos aBI
}
checkHornPos :: AS_BASIC.FORMULA -> AS_BASIC.FORMULA -> Bool
checkHornPos fc fl =
case fc of
AS_BASIC.Conjunction _ _ -> all isPosLiteral $ Tools.flatten fc
_ -> False
&&
isPosLiteral fl