{- |

Module : $Header$

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.

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 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 Common.AS_Annotation as AS_Anno

import qualified Propositional.Sign as Sign

import qualified QBF.Symbol as Symbol

import qualified QBF.Morphism as Morphism

import qualified Common.Lib.State as State

-- | types of propositional formulae

data QBFFormulae = PlainFormula -- Formula without structural constraints

| HornClause -- Horn Clause Formulae

deriving (Show, Eq, Ord)

-- | sublogics for propositional logic

data QBFSL = QBFSL

{

format :: QBFFormulae -- Structural restrictions

} deriving (Show, Eq, Ord)

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 :: QBFSL -> Sign.Sign -> Sign.Sign

prSig _ sig = sig

prMor :: QBFSL -> Morphism.Morphism -> Morphism.Morphism

prMor _ mor = mor

prSymMapM :: QBFSL

-> AS_BASIC.SYMBMAPITEMS

-> 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

-> [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

-> 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