{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-} -- | -- This module defines three altenative representations for certain propositional normal forms, namely -- -- > data XPDNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a -- > data XPCNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a -- > data MixForm a -- a type made of pairwise minimal DNF's and CNF's on a given atom type a -- -- For each of these types there is a converter from and a converter to propositional formulas -- -- > fromXPDNF :: Ord a => XPDNF a -> PropForm a toXPDNF :: Ord a => PropForm a -> XPDNF a -- > fromXPCNF :: Ord a => XPCNF a -> PropForm a toXPCNF :: Ord a => PropForm a -> XPCNF a -- > fromMixForm :: Ord a => MixForm a -> PropForm a toMixForm :: Ord a => PropForm a -> MixForm a -- -- Each of these three types is turned into a propositional algebra 'PropAlg', i.e. for every ordered type @a@ of /atoms/ -- we have three instances -- -- > PropAlg a (XPDNF a) -- > PropAlg a (XPCNF a) -- > PropAlg a (MixForm a) -- -- Different to the two default propositional algebras on propositional formulas and truth tables, these three algebras comprise fast -- function implementations and thus provide practical versions for propositional algebras, where propositions of arbitrary size -- are processed in reasonable time. -- In more detail the involved complexities are given in the table below (see ......). -- It also explains, which of the three algebras should be chosen in an actual application. -- -- Actually, this module is essentially a re-implementation of already explained concepts from "PropLogicCore" and "DefaultPropLogic" -- and for the user it shouldn't be necessary to further explain how the algorithms work. -- The remainder of this document is an attempt to do just that. -- However, if you at least want an idea of what is going on here, it may suffice to read the first section with the introductory -- example below. {- This module defines three altenative representations for certain propositional normal forms, namely 'XPDNF' a representation for Prime Disjunctive Normal Forms 'DefaultPropLogic.PDNF', 'XPCNF' a representation for Prime Conjunctive Normal Forms 'DefaultPropLogic.PCNF', and 'MixForm' a type comprising pairwise minimal DNFs and CNFs. For each of these types there is a converter from and a converter to propositional formulas 'PropLogicCore.PropForm'. For example, for 'XPDNF' this is @fromXPDNF :: XPDNF a -> PropForm a@ and @toXPDNF :: PropForm a -> XPDNF a@. Each of these three types is turned into a propositional algebra, i.e. it becomes an instance of 'PropLogicCore.PropAlg'. Different to the two default propositional algebras on propositional formulas and truth tables (see 'DefaultPropLogic.PropForm' and 'DefaultPropLogic.TruthTable'), these three algebras comprise fast function implementations and thus provide practical versions for propositional algebras for propositions of any size, not just for formulas with very small atoms sets. -} module FastPropLogic ( -- * Introductory example -- ** Generating a Prime Disjunctive Normal Form, the default and the fast way -- | Recall, that we already defined /Disjunctive Normal Forms/ and /Prime Disjunctive Normal Forms/ in "DefaultPropLogic" as -- special versions of propositional formulas, along with a canonizer @pdnf@ to obtain these normal forms -- -- > type DNF a = PropForm a -- > type PDNF a = DNF a -- > pdnf :: PropForm a -> PDNF a -- -- For a simple example formula @p@, given by -- -- > > p = DJ [EJ [A "x", A "y"], N (A "z")] :: PropForm String -- -- more conveniently displayed by -- -- > > display p -- > [[x <-> y] + -z] -- -- the PDNF of @p@ is then generated by -- -- > > pdnf p -- > DJ [CJ [EJ [A "x",F],EJ [A "y",F]],CJ [EJ [A "x",T],EJ [A "y",T]],CJ [EJ [A "z",F]]] -- > > display (pdnf p) -- > [[[x <-> false] * [y <-> false]] + [[x <-> true] * [y <-> true]] + [* [z <-> false]]] -- -- or more conveniently displayed in its evaluated form -- -- > > display (eval (pdnf p)) -- > [[-x * -y] + [x * y] + -z] -- -- .............!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!.............................. -- -- (Actually, each converter pair is also part of each of the given algebras. For example, in the XPDNF instance holds: -- 'fromXPDNF' = 'toPropForm' and 'toXPDNF' = 'fromPropForm'.) -- -- ** XPDNF as a propositional algebra -- -- | ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,, -- ** The canonization steps -- -- * Syntax IAtom, ILit, ILine, IForm, XLit, XLine, XForm, XPDNF(..), XPCNF(..), MixForm(..), -- * Conversions -- ** IdxPropForm -- indexed propositional formulas IdxPropForm, tr, -- | @tr f form@ replaces each atom form occurrence @(A x)@ in the formula @form@ by the new atom @(A (f x))@. Everything else remains. iTr, -- | @iTr [i_1,...,i_n] iform@ replaces each index @j@ in @iform@ by @i_j@. For example, -- -- > > let iform = iForm [[-1,3,-4,5],[-2,-3,4,6]] :: IForm -- > > iform -- > COSTACK [COSTACK [-1,3,-4,5],COSTACK [-2,-3,4,6]] -- > > iTr [7,8,9,10,11,12,13] iform -- > COSTACK [COSTACK [-7,9,-10,11],COSTACK [-8,-9,10,12]] -- > > iTr [2,4] iform -- > -- error, because the index list [2,4] must at least be of length 6 to cover the indices 1,..,6 of iform. idx, -- | @idx [i_1,...,i_n] i_k@ returns @k@, i.e. the index of the index in the given index list. -- Note, that the first member of the list starts with index 1, not 0. For example, -- -- > > idx [2,4,6,8] 6 -- > 3 nth, -- | @nth [i_1,...,i_n] k@ returns @i_k@, i.e. the @k@'s element in the list @[i_1,...,i_n]@, counting from @1@. For example, -- -- > > nth [2,4,6,8] 3 -- > 6 itr, iUni, unifyIdxPropForms, unifyXForms, fromIdxPropForm, toIdxPropForm, newAtomsXForm, -- ** Purely syntactical conversions to propositional formulas iLIT, iNLC, iNLD, iCNF, iDNF, xLIT, xNLC, xNLD, xCNF, xDNF, -- ** Conversions to and from propositional formulas toXPDNF, toXPCNF, toM2DNF, toM2CNF, fromXPDNF, fromXPCNF, fromMixForm, -- * The IForm algebra -- ** Basic operations isIAtom, isILit, isILine, isIForm, iLine, iForm, iAtom, iBool, negLit, lineIndices, formIndices, lineLength, formLength, volume, isOrderedForm, orderForm, -- ** The propositional algebra operations atomForm, botForm, topForm, formJoinForm, formListJoin, lineMeetLine, lineMeetForm, formMeetForm, formListMeet, dualLine, dualForm, invertLine, invertForm, negLine, negForm, formCojoinLine, formCojoinForm, formAntijoinLine, formAntijoinForm, elimLine, elimForm, lineCovLine, lineCovForm, formCovForm, -- ** Generation of pairwise minimal, minimal and prime forms -- *** Generation of prime and pairwise minimal forms of two lines pairPartition, CaseSymbol(..), caseSymbol, pairPrim', pairMin', xprim', xmin', xprim, xmin, pairPrim, pairMin, -- *** Implementation of the M- and the P-Procedure isMinimalPair, allPairs, isPairwiseMinimal, cPrime, cPrimes, mrec, m2form, iformJoinM2form, primForm, iformJoinPrimForm, -- * The XForm operations xformAtoms, xformRedAtoms, xformIrrAtoms, -- * The propositional algebras -- ** XPDNF and XPCNF -- ** MixForm mixToPDNF, mixToPCNF, -- * Complexities and choice of a algebra -- | -- -- > DefaultPropLogic. FastPropLogic -- > -------------------------------------- ----------------------------------- -- > PropForm TruthTable XPDNF XPCNF MixForm -- > -------------------------------------------------------------------------------------------------------------------------- -- > at -- > false -- > true -- > neg -- > conj, disj, subj, equij -- > valid -- > satisfiable -- > subvalent -- > equivalent -- > covalent, disvalent, -- > properSubvalent, properDisvalent -- > atoms -- > redAtoms, irrAtoms -- > nullatomic -- > subatomic, equiatomic -- > ......... -- > ......... ) where --------------------------------------------------------------------------------------------------------------- -- import import qualified Data.List as L import qualified TextDisplay as D import qualified Olist as O import qualified Costack as C import PropLogicCore import DefaultPropLogic (NegNormForm, negNormForm) -- the types type IAtom = Int -- I-Atom type IdxPropForm a = (O.Olist a, PropForm IAtom) -- indexed propositional formula -- type IntLitNormForm = PropForm ILit -- integer literal normal form type ILit = Int -- I-Literal or integer literal type type ILine = C.Costack ILit -- I-Line or integer line type type IForm = C.Costack ILine -- I-Form or integer form type type XLit a = (O.Olist a, ILit) -- X-Literal or indexed literal type type XLine a = (O.Olist a, ILine) -- X-Line or indexed line type type XForm a = (O.Olist a, IForm) -- X-Form or indexed form type data XPDNF a = XPDNF (XForm a) -- Indexed/Extended Prime Disjunctive Normal Forms deriving (Show, Read, Eq) data XPCNF a = XPCNF (XForm a) -- Indexed/Extended Prime Conjunctive Normal Forms deriving (Show, Read, Eq) data MixForm a -- Mixed Forms: = M2DNF (XForm a) -- Pairwise Minimal Disjunctive Normal Forms | M2CNF (XForm a) -- Pairwise Minimal Conjunctive Normal Forms | PDNF (XForm a) -- Prime Disjunctive Normal Forms | PCNF (XForm a) -- Prime Conjunctive Normal Forms deriving (Show, Read, Eq) -- display instance D.Display IForm where textFrame form = textframe where indices = formIndices form oneRow line iL = if C.isEmpty line then if null iL then [] else [""] : (oneRow line (Prelude.tail iL)) else case compare (iAtom (C.head line)) (Prelude.head iL) of GT -> [""] : (oneRow line (Prelude.tail iL)) EQ -> if iBool (C.head line) then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL)) else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL)) frameTable = map (\ line -> oneRow line indices) (C.toList form) textframe = D.gridMerge (D.normalTextFrameTable frameTable) instance D.Display a => D.Display (XForm a) where textFrame (aL, form) = textframe where headRow = map D.textFrame aL indices = [1..(length aL)] :: [IAtom] oneRow line iL = if C.isEmpty line then if null iL then [] else [""] : (oneRow line (Prelude.tail iL)) else case compare (iAtom (C.head line)) (Prelude.head iL) of GT -> [""] : (oneRow line (Prelude.tail iL)) EQ -> if iBool (C.head line) then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL)) else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL)) tableBody = map (\ line -> oneRow line indices) (C.toList form) textframe = D.gridMerge (D.normalTextFrameTable (headRow:tableBody)) titledTextFrame :: D.Display a => (String,String,String) -> XForm a -> D.TextFrame titledTextFrame (empty, full, title) (aL,iform) = if null aL then if C.isEmpty iform then D.textFrameBox (D.correctTextFrame [title,empty]) else D.textFrameBox (D.correctTextFrame [title,full]) else let body = D.textFrame (aL,iform) textframe = D.textFrameBox (D.plainMerge (D.normalTextFrameTable [[[title]],[body]])) in textframe instance D.Display a => D.Display (XPDNF a) where textFrame (XPDNF xform) = titledTextFrame ("false", "true", "XPDNF") xform instance D.Display a => D.Display (XPCNF a) where textFrame (XPCNF xform) = titledTextFrame ("true", "false", "XPCNF") xform instance D.Display a => D.Display (MixForm a) where textFrame (M2DNF xform) = titledTextFrame ("false", "true", "M2DNF") xform textFrame (M2CNF xform) = titledTextFrame ("true", "false", "M2CNF") xform textFrame (PDNF xform) = titledTextFrame ("false", "true", "PDNF") xform textFrame (PCNF xform) = titledTextFrame ("true", "false", "PCNF") xform -- order instance Ord ILine where compare left right = if C.isEmpty left then if C.isEmpty right then EQ else LT else if C.isEmpty right then GT else case compare (iAtom (C.head left)) (iAtom (C.head right)) of LT -> LT GT -> GT EQ -> case compare (iBool (C.head left)) (iBool (C.head right)) of LT -> LT GT -> GT EQ -> compare (C.tail left) (C.tail right) instance Ord IForm where compare form1 form2 = if C.isEmpty form1 then if C.isEmpty form2 then EQ else LT else if C.isEmpty form2 then GT else case compare (C.head form1) (C.head form2) of LT -> LT GT -> GT EQ -> compare (C.tail form1) (C.tail form2) -- convertions via IntLitNormForm toXPDNF :: Ord a => PropForm a -> XPDNF a toXPDNF p = XPDNF (aL, primForm iform) where (aL, iprop) = toIdxPropForm p iform = fromNegNF (negNormForm iprop) fromNegNF (A n) = atomForm n fromNegNF (N (A n)) = atomForm (negLit n) fromNegNF F = botForm fromNegNF T = topForm fromNegNF (CJ pL) = formListMeet (map fromNegNF pL) fromNegNF (DJ pL) = formListJoin (map fromNegNF pL) toXPCNF :: Ord a => PropForm a -> XPCNF a toXPCNF p = XPCNF (aL, primForm iform) where (aL, iprop) = toIdxPropForm p iform = fromNegNF (negNormForm iprop) fromNegNF (A n) = atomForm n fromNegNF (N (A n)) = atomForm (negLit n) fromNegNF F = topForm fromNegNF T = botForm fromNegNF (CJ pL) = formListJoin (map fromNegNF pL) fromNegNF (DJ pL) = formListMeet (map fromNegNF pL) fromXPDNF :: Ord a => XPDNF a -> PropForm a fromXPDNF (XPDNF xform) = xDNF xform fromXPCNF :: Ord a => XPCNF a -> PropForm a fromXPCNF (XPCNF xform) = xCNF xform toM2DNF :: Ord a => PropForm a -> MixForm a toM2DNF p = M2DNF (aL, m2form iform) where (aL, iprop) = toIdxPropForm p iform = fromIntLitNormForm (negNormForm iprop) fromIntLitNormForm (A n) = atomForm n fromIntLitNormForm F = botForm fromIntLitNormForm T = topForm fromIntLitNormForm (CJ pL) = formListMeet (map fromIntLitNormForm pL) fromIntLitNormForm (DJ pL) = formListJoin (map fromIntLitNormForm pL) toM2CNF :: Ord a => PropForm a -> MixForm a toM2CNF p = M2CNF (aL, m2form iform) where (aL, iprop) = toIdxPropForm p iform = fromIntLitNormForm (negNormForm iprop) fromIntLitNormForm (A n) = atomForm n fromIntLitNormForm F = topForm fromIntLitNormForm T = botForm fromIntLitNormForm (CJ pL) = formListJoin (map fromIntLitNormForm pL) fromIntLitNormForm (DJ pL) = formListMeet (map fromIntLitNormForm pL) fromMixForm :: Ord a => MixForm a -> PropForm a fromMixForm (M2DNF xform) = xDNF xform fromMixForm (M2CNF xform) = xCNF xform fromMixForm (PDNF xform) = xDNF xform fromMixForm (PCNF xform) = xCNF xform -- translations, indices and unifications tr :: (s -> t) -> PropForm s -> PropForm t tr f (A x) = A (f x) tr f F = F tr f T = T tr f (N prop) = N (tr f prop) tr f (CJ propL) = CJ (map (tr f) propL) tr f (DJ propL) = DJ (map (tr f) propL) tr f (SJ propL) = SJ (map (tr f) propL) tr f (EJ propL) = EJ (map (tr f) propL) iTr :: O.Olist IAtom -> IForm -> IForm iTr aL form = C.map (iTr' aL 1) form where iTr' aL n line = if C.isEmpty line then line else case compare n (iAtom (C.head line)) of EQ -> if (iBool (C.head line)) then C.cons (head aL) (iTr' (tail aL) (n + 1) (C.tail line)) else C.cons (negLit (head aL)) (iTr' (tail aL) (n + 1) (C.tail line)) LT -> iTr' (tail aL) (n + 1) line idx :: Ord a => O.Olist a -> a -> IAtom idx [] x = error "idx -- empty list" idx (y:yL) x = case compare y x of LT -> 1 + (idx yL x) EQ -> 1 GT -> error "idx -- atom is not a list member" nth :: Ord a => O.Olist a -> IAtom -> a nth oli n = if n < 1 then error ("nth -- undefined IAtom " ++ (show n)) else iter (n, oli) where iter (i, []) = error ("nth -- index " ++ (show n) ++ " exceeds the list length") iter (i, (x:xL)) = if i == 1 then x else iter (i - 1, xL) itr :: Ord a => O.Olist a -> O.Olist a -> Maybe (O.Olist IAtom) itr s1 s2 = iter True s1 s2 1 [] -- True means that s1 == s2 where iter b [] [] n nL = if b then Nothing else (Just (reverse nL)) iter b [] (y:yL) n nL = iter False [] yL (n + 1) nL iter b (x:xL) (y:yL) n nL = case compare x y of EQ -> iter b xL yL (n + 1) (n:nL) GT -> iter False (x:xL) yL (n + 1) nL LT -> error "itr -- first list is not included by second list" iUni :: Ord a => [O.Olist a] -> (O.Olist a, [Maybe (O.Olist IAtom)]) iUni sL = (aL, map (\ s -> itr s aL) sL) where aL = O.unionList sL unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (O.Olist a, [PropForm IAtom]) unifyIdxPropForms pL = (aL, ipropL) where (aL, maybeL) = iUni (map fst pL) update (iprop, Nothing) = iprop update (iprop, Just iL) = tr (nth iL) iprop ipropL = map update (zip (map snd pL) maybeL) unifyXForms :: Ord a => [XForm a] -> (O.Olist a, [IForm]) unifyXForms xformL = (aL, iformL) where (aL, maybeL) = iUni (map fst xformL) update (iform, Nothing) = iform update (iform, Just iL) = iTr iL iform iformL = map update (zip (map snd xformL) maybeL) newAtomsXForm :: Ord a => XForm a -> O.Olist a -> XForm a newAtomsXForm (oldAts, iform) newAts = (newAts, updateIForm (updateList oldAts newAts) iform) where updateList :: Ord a => O.Olist a -> O.Olist a -> [Maybe IAtom] updateList oldAts newAts = updateList' oldAts 1 newAts where updateList' [] n newAts = [] updateList' (x:xL) n [] = L.replicate (length (x:xL)) Nothing updateList' (x:xL) n (y:yL) = case compare x y of LT -> Nothing : (updateList' xL n (y:yL)) EQ -> (Just n) : (updateList' xL (n + 1) yL) GT -> updateList' (x:xL) (n + 1) yL updateIForm :: [Maybe IAtom] -> IForm -> IForm updateIForm maL iform = C.map (updateILine maL) iform updateILine :: [Maybe IAtom] -> ILine -> ILine updateILine maL iline = updateILine' 1 maL iline where updateILine' _ [] _ = C.empty updateILine' n (x:xL) iline = if C.isEmpty iline then iline else case compare n (iAtom (C.head iline)) of LT -> updateILine' (n + 1) xL iline EQ -> case x of Nothing -> updateILine' (n + 1) xL (C.tail iline) Just i -> if iBool (C.head iline) then C.cons i (updateILine' (n + 1) xL (C.tail iline)) else C.cons (negLit i) (updateILine' (n + 1) xL (C.tail iline)) -- X-Prop conversions fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a fromIdxPropForm (s, iprop) = tr (nth s) iprop toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a toIdxPropForm prop = (s, tr (idx s) prop) where s = propFormAtoms prop propFormAtoms :: Ord a => PropForm a -> O.Olist a propFormAtoms p = case p of (A a) -> [a] F -> [] T -> [] (N p) -> propFormAtoms p (CJ pL) -> O.unionList (map propFormAtoms pL) (DJ pL) -> O.unionList (map propFormAtoms pL) (SJ pL) -> O.unionList (map propFormAtoms pL) (EJ pL) -> O.unionList (map propFormAtoms pL) -- I-Form conversion iLIT :: ILit -> PropForm IAtom iLIT l | l < 0 = N (A (negLit l)) | l > 0 = A l | otherwise = error "iLIT -- zero literal" iNLC :: ILine -> PropForm IAtom iNLC line = CJ (map iLIT (C.toList line)) iNLD :: ILine -> PropForm IAtom iNLD line = DJ (map iLIT (C.toList line)) iCNF :: IForm -> PropForm IAtom iCNF form = CJ (map iNLD (C.toList form)) iDNF :: IForm -> PropForm IAtom iDNF form = DJ (map iNLC (C.toList form)) -- X-Form conversion xLIT :: Ord a => XLit a -> PropForm a xLIT (s, l) = fromIdxPropForm (s, iLIT l) xNLC :: Ord a => XLine a -> PropForm a xNLC (s, line) = fromIdxPropForm (s, iNLC line) xNLD :: Ord a => XLine a -> PropForm a xNLD (s, line) = fromIdxPropForm (s, iNLD line) xCNF :: Ord a => XForm a -> PropForm a xCNF (s, form) = fromIdxPropForm (s, iCNF form) xDNF :: Ord a => XForm a -> PropForm a xDNF (s, form) = fromIdxPropForm (s, iDNF form) -- type correctness and type constructors isIAtom :: Int -> Bool isIAtom n = n > 0 isILit :: Int -> Bool isILit n = n /= 0 isILine :: C.Costack Int -> Bool isILine x = iter (C.toList x) where iter [] = True iter [n] = isILit(n) iter (n1:n2:nL) = isILit(n1) && iAtom(n1) < iAtom(n2) && iter(n2:nL) isIForm :: C.Costack (C.Costack Int) -> Bool isIForm x = iter (C.toList x) where iter [] = True iter (c:cL) = (isILine c) && iter cL iLine :: [Int] -> ILine iLine iL = C.fromList (iter (zeroCheck iL)) where iter [] = [] iter [i] = [i] iter (j:i:iL) = if (abs j) < (abs i) then j:(iter (i:iL)) else error ("IForm.iLine -- in literal order " ++ (show j) ++ " is not before " ++ (show i)) zeroCheck [] = [] zeroCheck (i:iL) = if i == 0 then error "Iform.iLine -- there is a 0 in the list" else i:(zeroCheck iL) iForm :: [[Int]] -> IForm iForm iLL = C.fromList (map iLine iLL) -- literal operations iAtom :: ILit -> IAtom iAtom = abs iBool :: ILit -> Bool iBool l | l < 0 = False | l > 0 = True | l == 0 = error "IForm.iBool -- zero literal integer" negLit :: ILit -> ILit negLit = Prelude.negate -- index lists lineIndices :: ILine -> O.Olist IAtom lineIndices line = map iAtom (C.toList line) formIndices :: IForm -> O.Olist IAtom formIndices form = O.unionList (C.toList (C.map lineIndices form)) -- syntactic sizes lineLength :: ILine -> Int lineLength = C.length formLength :: IForm -> Int formLength = C.length volume :: IForm -> Int volume form = C.foldr (+) 0 (C.map lineLength form) -- ordered forms isOrderedForm :: IForm -> Bool isOrderedForm form = C.strictSorted form orderForm :: IForm -> IForm orderForm form = C.strictSort form -- the propositional algebra operations atomForm :: IAtom -> IForm atomForm atom = C.singleton (C.singleton atom) botForm :: IForm botForm = C.empty topForm :: IForm topForm = C.singleton C.empty formJoinForm :: IForm -> IForm -> IForm formJoinForm form1 form2 = C.append form1 form2 formListJoin :: [IForm] -> IForm formListJoin formL = C.concat formL lineMeetLine :: ILine -> ILine -> IForm lineMeetLine line1 line2 = jrec (line1, line2, C.empty) where jrec (first, second, third) = if C.isEmpty first then C.singleton (C.append third second) else if C.isEmpty second then C.singleton (C.append third first) else case compare (iAtom (C.head first)) (iAtom (C.head second)) of LT -> jrec (C.tail first, second, C.cocons third (C.head first)) GT -> jrec (first, C.tail second, C.cocons third (C.head second)) EQ -> if (iBool (C.head first)) == (iBool (C.head second)) then jrec (C.tail first, C.tail second, C.cocons third (C.head first)) else C.empty lineMeetForm :: ILine -> IForm -> IForm lineMeetForm line form = formListJoin (map (lineMeetLine line) (C.toList form)) formMeetForm :: IForm -> IForm -> IForm formMeetForm form1 form2 = formListJoin (map (\ line -> lineMeetForm line form2) (C.toList form1)) formListMeet :: [IForm] -> IForm formListMeet [] = C.singleton C.empty formListMeet [form] = form formListMeet (form1:form2:formL) = formListMeet ((formMeetForm form1 form2) : formL) dualLine :: ILine -> IForm dualLine line = C.map C.singleton line dualForm :: IForm -> IForm dualForm form = formListMeet (map dualLine (C.toList form)) invertLine :: ILine -> ILine invertLine = C.map negLit invertForm :: IForm -> IForm invertForm = C.map invertLine negLine :: ILine -> IForm negLine line = C.map (\ l -> (C.singleton (negLit l))) line negForm :: IForm -> IForm negForm form = formListMeet (map negLine (C.toList form)) formCojoinLine :: IForm -> ILine -> IForm formCojoinLine form line = formJoinForm form (dualLine line) formCojoinForm :: IForm -> IForm -> IForm formCojoinForm form1 form2 = formListMeet (C.toList (C.map (formCojoinLine form1) form2)) formAntijoinLine :: IForm -> ILine -> IForm formAntijoinLine form line = formJoinForm form (negLine line) formAntijoinForm :: IForm -> IForm -> IForm formAntijoinForm form1 form2 = formListMeet (C.toList (C.map (formAntijoinLine form1) form2)) elimLine :: ILine -> O.Olist IAtom -> ILine elimLine line aL | C.isEmpty line = C.empty | O.isEmpty aL = line | otherwise = case compare (iAtom (C.head line)) (head aL) of LT -> C.cons (C.head line) (elimLine (C.tail line) aL) GT -> elimLine line (tail aL) EQ -> elimLine (C.tail line) (tail aL) elimForm :: IForm -> O.Olist IAtom -> IForm elimForm form aL = C.map (\ line -> (elimLine line aL)) form lineCovLine :: ILine -> ILine -> Bool lineCovLine line1 line2 | C.isEmpty line2 = True | C.isEmpty line1 = False | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of LT -> lineCovLine (C.tail line1) line2 GT -> False EQ -> if (iBool (C.head line1)) == (iBool (C.head line2)) then lineCovLine (C.tail line1) (C.tail line2) else False lineCovForm :: ILine -> IForm -> Bool lineCovForm line form = if C.isEmpty form then False else if lineCovLine line (C.head form) then True else lineCovForm line (C.tail form) formCovForm :: IForm -> IForm -> Bool formCovForm form1 form2 = if C.isEmpty form1 then True else if lineCovForm (C.head form1) form2 then formCovForm (C.tail form1) form2 else False -- Generation of the prime and minimal form of two lines pairPartition :: ILine -> ILine -> (ILine,ILine,ILine,ILine) pairPartition line1 line2 = iter (C.empty, C.empty, C.empty, C.empty, line1, line2) where iter :: (ILine,ILine,ILine,ILine,ILine,ILine) -> (ILine,ILine,ILine,ILine) iter (piL, rhoL, sigmaL, tauL, line1, line2) = if C.isEmpty line1 then (piL, rhoL, sigmaL, C.append tauL line2) else if C.isEmpty line2 then (piL, rhoL, C.append sigmaL line1, tauL) else case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of LT -> iter (piL, rhoL, C.cocons sigmaL (C.head line1), tauL, C.tail line1, line2) GT -> iter (piL, rhoL, sigmaL, C.cocons tauL (C.head line2), line1, C.tail line2) EQ -> if iBool (C.head line1) == iBool (C.head line2) then iter (C.cocons piL (C.head line1), rhoL, sigmaL, tauL, C.tail line1, C.tail line2) else iter (piL, C.cocons rhoL (C.head line1), sigmaL, tauL, C.tail line1, C.tail line2) data CaseSymbol = NOOO | NOOP | NOPO | NOPP | NIOO | NIOP | NIPO | NIPP | NMNN deriving (Show, Read, Eq, Ord) caseSymbol :: ILine -> ILine -> CaseSymbol caseSymbol left right | p >= 0 && r == 0 && s == 0 && t == 0 = NOOO | p >= 0 && r == 0 && s == 0 && t >= 1 = NOOP | p >= 0 && r == 0 && s >= 1 && t == 0 = NOPO | p >= 0 && r == 0 && s >= 1 && t >= 1 = NOPP | p >= 0 && r == 1 && s == 0 && t == 0 = NIOO | p >= 0 && r == 1 && s == 0 && t >= 1 = NIOP | p >= 0 && r == 1 && s >= 1 && t == 0 = NIPO | p >= 0 && r == 1 && s >= 1 && t >= 1 = NIPP | p >= 0 && r >= 2 && s >= 0 && t >= 0 = NMNN where (piL, rhoL, sigmaL, tauL) = pairPartition left right (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL) -- First version pairPrim' :: ILine -> ILine -> IForm pairPrim' left right | p >= 0 && r == 0 && s == 0 && t == 0 = C.singleton left | p >= 0 && r == 0 && s == 0 && t >= 1 = C.singleton left | p >= 0 && r == 0 && s >= 1 && t == 0 = C.singleton right | p >= 0 && r == 0 && s >= 1 && t >= 1 = C.fromList [left,right] | p >= 0 && r == 1 && s == 0 && t == 0 = C.singleton piL | p >= 0 && r == 1 && s == 0 && t >= 1 = C.fromList [left, lineMerge piL tauL] | p >= 0 && r == 1 && s >= 1 && t == 0 = C.fromList [lineMerge piL sigmaL, right] | p >= 0 && r == 1 && s >= 1 && t >= 1 = C.fromList [left, right, lineMerge piL (lineMerge sigmaL tauL)] | p >= 0 && r >= 2 && s >= 0 && t >= 0 = C.fromList [left, right] where (piL, rhoL, sigmaL, tauL) = pairPartition left right (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL) lineMerge line1 line2 | C.isEmpty line1 = line2 | C.isEmpty line2 = line1 | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of LT -> C.cons (C.head line1) (lineMerge (C.tail line1) line2) GT -> C.cons (C.head line2) (lineMerge line1 (C.tail line2)) pairMin' :: ILine -> ILine -> IForm pairMin' left right = C.take 2 (pairPrim' left right) xprim' :: ILine -> ILine -> (CaseSymbol, IForm) xprim' left right = (caseSymbol left right, pairPrim' left right) xmin' :: ILine -> ILine -> (CaseSymbol, IForm) xmin' left right = (caseSymbol left right, pairMin' left right) -- Second, fast and final version xprim :: ILine -> ILine -> (CaseSymbol, IForm) xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0) where xprec (left, left', right, right', c1, c2, c3, r, s, t) | r > 1 = (NMNN, C.fromList [C.append left left', C.append right right']) | C.isEmpty left' && r == 0 && s == 0 && C.isEmpty right' && t == 0 = (NOOO, C.singleton left) | C.isEmpty left' && r == 0 && s == 0 = (NOOP, C.singleton left) | C.isEmpty left' && r == 0 && s > 0 && C.isEmpty right' && t == 0 = (NOPO, C.singleton right) | C.isEmpty left' && r == 0 && s > 0 = (NOPP, C.fromList [left, C.append right right']) | C.isEmpty left' && r == 1 && s == 0 && C.isEmpty right' && t == 0 = (NIOO, C.singleton c1) | C.isEmpty left' && r == 1 && s == 0 = (NIOP, C.fromList [left, C.append c2 right']) | C.isEmpty left' && r == 1 && s > 0 && C.isEmpty right' && t == 0 = (NIPO, C.fromList [c1, C.append right right']) | C.isEmpty left' && r == 1 && s > 0 = (NIPP, C.fromList [left, C.append right right', C.append c3 right']) | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t == 0 = (NOPO, C.singleton right) | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t > 0 = (NOPP, C.fromList [C.append left left', right]) | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t == 0 = (NIPO, C.fromList [C.append c1 left', right]) | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t > 0 = (NIPP, C.fromList [C.append left left', right, C.append c3 left']) | not (C.isEmpty left') && not (C.isEmpty right') = let x = C.head left' y = C.head right' in case compare (iAtom x) (iAtom y) of LT -> xprec (C.cocons left x, C.tail left', right, right', C.cocons c1 x, c2, C.cocons c3 x, r, s + 1, t) GT -> xprec (left, left', C.cocons right y, C.tail right', c1, C.cocons c2 y, C.cocons c3 y, r, s, t + 1) EQ -> if iBool x == iBool y then xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right', C.cocons c1 x, C.cocons c2 y, C.cocons c3 y, r, s, t) else xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right', c1, c2, c3, r + 1, s, t) {-- old version of xprim xprim :: ILine -> ILine -> (CaseSymbol, IForm) xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0) where xprec (left, left', right, right', cboth, cleft, cright, r, s, t) = if r > 1 then (NMNN, C.fromList [C.append left left', C.append right right']) else if C.isEmpty left' then if r == 0 then if s == 0 then if (C.isEmpty right' && t == 0) then (NOOO, C.singleton left) else (NOOP, C.singleton left) else if (C.isEmpty right' && t == 0) then (NOPO, C.singleton right) else (NOPP, C.fromList [left, C.append right right']) else if s == 0 then if (C.isEmpty right' && t == 0) then (NIOO, C.singleton cboth) else (NIOP, C.fromList [left, C.append cleft right']) else if (C.isEmpty right' && t == 0) then (NIPO, C.fromList [cboth, C.append right right']) else (NIPP, C.fromList [cboth, C.append right right', C.append cright right']) else if C.isEmpty right' then if r == 0 then if t == 0 then (NOPO, C.singleton right) else (NOPP, C.fromList [C.append left left', right]) else if t == 0 then (NIPO, C.fromList [C.append cboth left', right]) else (NIPP, C.fromList [C.append left left', right, C.append cright left']) else case compare (iAtom (C.head left')) (iAtom (C.head right')) of LT -> xprec ( C.cocons left (C.head left'), C.tail left', right, right', C.cocons cboth (C.head left'), cleft, C.cocons cright (C.head left'), r, s+1, t) GT -> xprec ( left, left', C.cocons right (C.head right'), C.tail right', cboth, C.cocons cleft (C.head right'), C.cocons cright (C.head right'), r, s, t+1) EQ -> if iBool (C.head left') == iBool (C.head right') then xprec ( C.cocons left (C.head left'), C.tail left', C.cocons right (C.head right'), C.tail right', C.cocons cboth (C.head left'), C.cocons cleft (C.head left'), C.cocons cright (C.head right'), r, s, t) else xprec ( C.cocons left (C.head left'), C.tail left', C.cocons right (C.head right'), C.tail right', cboth, cleft, cright, r+1, s, t) --} xmin :: ILine -> ILine -> (CaseSymbol, IForm) xmin left right = case xprim left right of (NIPP, form) -> (NIPP, C.take 2 form) (symb, form) -> (symb, form) pairPrim :: ILine -> ILine -> IForm pairPrim left right = snd (xprim left right) pairMin :: ILine -> ILine -> IForm pairMin left right = snd (xmin left right) -- Pairwise minimality and complementary prime list isMinimalPair :: ILine -> ILine -> Bool isMinimalPair left right = [left, right] == C.toList (pairMin' left right) allPairs :: [a] -> [(a,a)] allPairs [] = [] allPairs [x] = [] allPairs (x:xL) = (iter x xL) ++ (allPairs xL) where iter x [] = [] iter x (y:yL) = (x,y):(iter x yL) isPairwiseMinimal :: IForm -> Bool isPairwiseMinimal form = Prelude.all isMinPair (allPairs (C.toList form)) where isMinPair (x,y) = isMinimalPair x y -- C-Primes cPrime :: ILine -> ILine -> Maybe ILine cPrime left right = case xprim left right of (NIPP, form) -> Just (C.head (C.tail (C.tail form))) (symb, form) -> Nothing cPrimes :: IForm -> IForm cPrimes form = C.fromList (concat (map cp (allPairs (C.toList form)))) where cp (left ,right) = case cPrime left right of Just line -> [line] Nothing -> [] -- The M-Procedure and functions with pairwise minimal IForm results mrec :: (IForm,IForm,IForm) -> IForm mrec (gammaL, muL, muL') = if C.isEmpty gammaL then C.append muL muL' else if C.isEmpty muL' then mrec (C.tail gammaL, C.empty, C.cons (C.head gammaL) muL) else case xmin (C.head gammaL) (C.head muL') of (NOOO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL') (NOOP, pp) -> mrec (C.append (C.tail gammaL) (C.tail muL'), C.empty, C.cons (C.head gammaL) muL) (NOPO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL') (NOPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL') (NIOO, pp) -> mrec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL')) (NIOP, pp) -> mrec (C.concat [C.tail gammaL, C.tail pp, C.tail muL'], C.empty, C.cons (C.head gammaL) muL) (NIPO, pp) -> mrec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL') (NIPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL') (NMNN, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL') m2form :: IForm -> IForm m2form form = mrec (form, C.empty, C.empty) iformJoinM2form :: IForm -> IForm -> IForm iformJoinM2form iform m2form = mrec (iform, C.empty, m2form) -- The P-Procedure and functions with prime IForm results primFormFromOrdM2form :: IForm -> IForm primFormFromOrdM2form ordM2form = let ordM2form' = orderForm (iformJoinM2form (cPrimes ordM2form) ordM2form) in if ordM2form' == ordM2form then ordM2form' else primFormFromOrdM2form ordM2form' primForm :: IForm -> IForm primForm iform = primFormFromOrdM2form $ orderForm $ m2form iform iformJoinPrimForm :: IForm -> IForm -> IForm iformJoinPrimForm iform pform = primFormFromOrdM2form $ orderForm $ iformJoinM2form iform pform {-- the following prec, primform, ordPrimForm are obsolete ----------------------------------------------------------- prec :: (IForm, IForm, IForm, IForm) -> IForm prec (gammaL, muL, muL', piL) | C.isEmpty gammaL && C.isEmpty piL = C.append muL muL' | C.isEmpty gammaL = prec (piL, C.empty, C.append muL muL', C.empty) | C.isEmpty muL' = prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty) | otherwise = case xprim (C.head gammaL) (C.head muL') of (NOOO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty) (NOOP, pp) -> prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty) (NOPO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty) (NOPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL) (NIOO, pp) -> prec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'), C.empty) (NIOP, pp) -> prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty) (NIPO, pp) -> prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty) (NIPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL) (NMNN, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL) -- OLD VERSION -------- prec :: (IForm, IForm, IForm, IForm) -> IForm prec (gammaL, muL, muL', piL) = if C.isEmpty gammaL then if C.isEmpty piL then C.append muL muL' else prec (piL, C.empty, C.append muL muL', C.empty) else if C.isEmpty muL' then prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty) else case xprim (C.head gammaL) (C.head muL') of (NOOO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty) (NOOP, pp) -> prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty) (NOPO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty) (NOPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL) (NIOO, pp) -> -- old version: --!! -- prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty) prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL (C.tail muL'), C.empty) (NIOP, pp) -> prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty) (NIPO, pp) -> prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty) (NIPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL) (NMNN, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL) primForm :: IForm -> IForm primForm form = prec (form, C.empty, C.empty, C.empty) ordPrimForm :: IForm -> IForm ordPrimForm = orderForm . primForm ------------------------------------------------------------------------------------------------------------------} -- XForm operations xformAtoms :: Ord a => XForm a -> O.Olist a xformAtoms (aL,iform) = aL xformRedAtoms :: Ord a => XForm a -> O.Olist a xformRedAtoms xform = O.difference (xformAtoms xform) (xformIrrAtoms xform) xformIrrAtoms :: Ord a => XForm a -> O.Olist a xformIrrAtoms (aL, iform) = iter aL 1 (formIndices iform) where iter aL n [] = [] iter (a:aL) n (i:iL) = case compare n i of EQ -> a : (iter aL (n + 1) iL) LT -> iter aL (n + 1) (i:iL) -- The XPDNF algebra instance Ord a => PropAlg a (XPDNF a) where at x = XPDNF ([x], atomForm 1) false = XPDNF ([], botForm) true = XPDNF ([], topForm) neg (XPDNF (aL, iform)) = XPDNF (aL, primForm (negForm iform)) conj pL = XPDNF (aL, primForm (formListMeet iformL)) where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL) disj pL = XPDNF (aL, primForm (formListJoin iformL)) where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL) subj pL = XPDNF (aL, primForm (subj' iformL)) where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL) subj' [] = topForm subj' [iform] = topForm subj' (iform1:iform2:iformL) = formMeetForm (formJoinForm (negForm iform1) iform2) (subj' (iform2:iformL)) equij pL = XPDNF (aL, primForm (iform)) where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL) iform = formJoinForm (formListMeet iformL) (negForm (formListJoin iformL)) valid (XPDNF (aL, iform)) = iform == topForm satisfiable (XPDNF (aL, iform)) = iform /= botForm subvalent (XPDNF xform1) (XPDNF xform2) = formCovForm iform1 iform2 where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2] equivalent = (==) covalent p1 p2 = satisfiable (conj [p1, p2]) properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2 properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2 atoms (XPDNF xform) = xformAtoms xform redAtoms (XPDNF xform) = xformRedAtoms xform irrAtoms (XPDNF xform) = xformIrrAtoms xform ext (XPDNF (xL, iform)) yL = XPDNF (yL', primForm iform') where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL)) infRed (XPDNF (xL, iform)) yL = XPDNF (yL', iform''') where iform' = primForm (dualForm iform) (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL) iform''' = primForm (dualForm iform'') supRed (XPDNF xform) yL = XPDNF (yL', primForm iform') where (yL', iform') = newAtomsXForm xform (O.olist yL) infElim (XPDNF (xL, iform)) yL = infRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL)) supElim (XPDNF (xL, iform)) yL = supRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL)) toPropForm = fromXPDNF fromPropForm = toXPDNF instance Ord a => PropAlg a (XPCNF a) where at x = XPCNF ([x], atomForm 1) false = XPCNF ([], topForm) true = XPCNF ([], botForm) neg (XPCNF (aL, iform)) = XPCNF (aL, primForm (negForm iform)) conj pL = XPCNF (aL, primForm (formListJoin iformL)) where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL) disj pL = XPCNF (aL, primForm (formListMeet iformL)) where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL) subj pL = XPCNF (aL, primForm (subj' iformL)) where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL) subj' [] = botForm subj' [iform] = botForm subj' (iform1:iform2:iformL) = formJoinForm (formMeetForm (negForm iform1) iform2) (subj' (iform2:iformL)) equij pL = XPCNF (aL, primForm (iform)) where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL) iform = formMeetForm (formListJoin iformL) (negForm (formListMeet iformL)) valid (XPCNF (aL, iform)) = iform == botForm satisfiable (XPCNF (aL, iform)) = iform /= topForm subvalent (XPCNF xform1) (XPCNF xform2) = formCovForm iform2 iform1 where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2] equivalent = (==) covalent p1 p2 = satisfiable (conj [p1, p2]) properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2 properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2 atoms (XPCNF xform) = xformAtoms xform redAtoms (XPCNF xform) = xformRedAtoms xform irrAtoms (XPCNF xform) = xformIrrAtoms xform ext (XPCNF (xL, iform)) yL = XPCNF (yL', primForm iform') where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL)) infRed (XPCNF xform) yL = XPCNF (yL', primForm iform') where (yL', iform') = newAtomsXForm xform (O.olist yL) supRed (XPCNF (xL, iform)) yL = XPCNF (yL', iform''') where iform' = primForm (dualForm iform) (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL) iform''' = primForm (dualForm iform'') infElim (XPCNF (xL, iform)) yL = infRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL)) supElim (XPCNF (xL, iform)) yL = supRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL)) toPropForm = fromXPCNF fromPropForm = toXPCNF dualizeXPDNF :: Ord a => XPDNF a -> XPCNF a dualizeXPDNF (XPDNF (aL, iform)) = XPCNF (aL, primForm (dualForm iform)) dualizeXPCNF :: Ord a => XPCNF a -> XPDNF a dualizeXPCNF (XPCNF (aL, iform)) = XPDNF (aL, primForm (dualForm iform)) -- The MixForm algebra instance Ord a => PropAlg a (MixForm a) where at x = PDNF ([x], atomForm 1) -- alernatively = PCNF ([x], atomForm 1) false = PDNF ([], botForm) true = PCNF ([], botForm) neg (M2DNF (aL, iform)) = M2CNF (aL, invertForm iform) neg (M2CNF (aL, iform)) = M2DNF (aL, invertForm iform) neg (PDNF (aL, iform)) = PCNF (aL, invertForm iform) neg (PCNF (aL, iform)) = PDNF (aL, invertForm iform) conj [] = true conj [form] = form conj formL = M2CNF (aL, m2form (formListJoin iformL)) where (aL,iformL) = unifyXForms cnfL cnfL = map cnf formL cnf (M2CNF (aL,iform)) = (aL, iform) cnf (M2DNF (aL,iform)) = (aL, dualForm iform) cnf (PCNF (aL,iform)) = (aL, iform) cnf (PDNF (aL,iform)) = (aL, dualForm iform) disj [] = false disj [form] = form disj formL = M2DNF (aL, m2form (formListJoin iformL)) where (aL,iformL) = unifyXForms dnfL dnfL = map dnf formL dnf (M2CNF (aL,iform)) = (aL, dualForm iform) dnf (M2DNF (aL,iform)) = (aL, iform) dnf (PCNF (aL,iform)) = (aL, dualForm iform) dnf (PDNF (aL,iform)) = (aL, iform) subj [] = true subj [form] = PCNF (atoms form, botForm) subj formL = fromPropForm (SJ (map toPropForm formL)) equij [] = true equij [form] = PCNF (atoms form, botForm) equij formL = fromPropForm (EJ (map toPropForm formL)) valid (M2DNF (aL,iform)) = primForm iform == topForm valid (M2CNF (aL,iform)) = iform == botForm valid (PDNF (aL,iform)) = iform == topForm valid (PCNF (aL,iform)) = iform == botForm satisfiable (M2DNF (aL,iform)) = iform /= botForm satisfiable (M2CNF (aL,iform)) = primForm iform /= topForm satisfiable (PDNF (aL,iform)) = iform /= botForm satisfiable (PCNF (aL,iform)) = iform /= topForm subvalent form1 form2 = valid (subj [form1, form2]) equivalent form1 form2 = valid (equij [form1, form2]) covalent form1 form2 = satisfiable (conj [form1, form2]) properSubvalent form1 form2 = subvalent form1 form2 && not (equivalent form1 form2) properDisvalent form1 form2 = disvalent form1 form2 && satisfiable form1 && satisfiable form2 atoms (M2DNF (aL,iform)) = aL atoms (M2CNF (aL,iform)) = aL atoms (PDNF (aL,iform)) = aL atoms (PCNF (aL,iform)) = aL redAtoms (M2DNF (aL,iform)) = xformRedAtoms (aL, primForm iform) redAtoms (M2CNF (aL,iform)) = xformRedAtoms (aL, primForm iform) redAtoms (PDNF xform) = xformRedAtoms xform redAtoms (PCNF xform) = xformRedAtoms xform irrAtoms (M2DNF (aL,iform)) = xformIrrAtoms (aL, primForm iform) irrAtoms (M2CNF (aL,iform)) = xformIrrAtoms (aL, primForm iform) irrAtoms (PDNF xform) = xformIrrAtoms xform irrAtoms (PCNF xform) = xformIrrAtoms xform ext (M2DNF xform) aL = M2DNF (newAtomsXForm xform aL) ext (M2CNF xform) aL = M2CNF (newAtomsXForm xform aL) ext (PDNF xform) aL = PDNF (newAtomsXForm xform aL) ext (PCNF xform) aL = PCNF (newAtomsXForm xform aL) infRed form yL = M2CNF (yL', m2form iform') where (PCNF (xL, iform)) = mixToPCNF form (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL) supRed form yL = M2DNF (yL', m2form iform') where (PDNF (xL, iform)) = mixToPDNF form (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL) infElim form yL = infRed form (O.difference (atoms form) (O.olist yL)) supElim form yL = supRed form (O.difference (atoms form) (O.olist yL)) toPropForm = fromMixForm fromPropForm = toM2DNF -- alternatively: toM2CNF mixToPDNF :: Ord a => MixForm a -> MixForm a mixToPDNF (M2DNF (aL, iform)) = PDNF (aL, primForm iform) mixToPDNF (M2CNF (aL, iform)) = PDNF (aL, primForm (dualForm iform)) mixToPDNF (PDNF xform) = PDNF xform mixToPDNF (PCNF (aL, iform)) = PDNF (aL, primForm (dualForm iform)) mixToPCNF :: Ord a => MixForm a -> MixForm a mixToPCNF (M2DNF (aL, iform)) = PCNF (aL, primForm (dualForm iform)) mixToPCNF (M2CNF (aL, iform)) = PCNF (aL, primForm iform) mixToPCNF (PDNF (aL, iform)) = PCNF (aL, primForm (dualForm iform)) mixToPCNF (PCNF xform) = PCNF xform