| ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

Description | ||||||||||||||||||||||||||

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

Synopsis | ||||||||||||||||||||||||||

Introductory example | ||||||||||||||||||||||||||

Generating a Prime Disjunctive Normal Form, the default and the fast way | ||||||||||||||||||||||||||

Recall, that we already defined type DNF a = PropForm a type PDNF a = DNF a pdnf :: PropForm a -> PDNF a For a simple example formula > p = DJ [EJ [A "x", A "y"], N (A "z")] :: PropForm String more conveniently displayed by > display p [[x <-> y] + -z] the PDNF of > 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:
| ||||||||||||||||||||||||||

XPDNF as a propositional algebra | ||||||||||||||||||||||||||

,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,, | ||||||||||||||||||||||||||

The canonization steps | ||||||||||||||||||||||||||

Syntax | ||||||||||||||||||||||||||

type IAtom = Int | ||||||||||||||||||||||||||

type ILit = Int | ||||||||||||||||||||||||||

type ILine = Costack ILit | ||||||||||||||||||||||||||

type IForm = Costack ILine | ||||||||||||||||||||||||||

type XLit a = (Olist a, ILit) | ||||||||||||||||||||||||||

type XLine a = (Olist a, ILine) | ||||||||||||||||||||||||||

type XForm a = (Olist a, IForm) | ||||||||||||||||||||||||||

data XPDNF a | ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

data XPCNF a | ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

data MixForm a | ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

Conversions | ||||||||||||||||||||||||||

IdxPropForm -- indexed propositional formulas | ||||||||||||||||||||||||||

type IdxPropForm a = (Olist a, PropForm IAtom) | ||||||||||||||||||||||||||

tr :: (s -> t) -> PropForm s -> PropForm t | ||||||||||||||||||||||||||

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 :: Olist IAtom -> IForm -> IForm | ||||||||||||||||||||||||||

> 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 :: Ord a => Olist a -> a -> IAtom | ||||||||||||||||||||||||||

> idx [2,4,6,8] 6 3 | ||||||||||||||||||||||||||

nth :: Ord a => Olist a -> IAtom -> a | ||||||||||||||||||||||||||

> nth [2,4,6,8] 3 6 | ||||||||||||||||||||||||||

itr :: Ord a => Olist a -> Olist a -> Maybe (Olist IAtom) | ||||||||||||||||||||||||||

iUni :: Ord a => [Olist a] -> (Olist a, [Maybe (Olist IAtom)]) | ||||||||||||||||||||||||||

unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (Olist a, [PropForm IAtom]) | ||||||||||||||||||||||||||

unifyXForms :: Ord a => [XForm a] -> (Olist a, [IForm]) | ||||||||||||||||||||||||||

fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a | ||||||||||||||||||||||||||

toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a | ||||||||||||||||||||||||||

newAtomsXForm :: Ord a => XForm a -> Olist a -> XForm a | ||||||||||||||||||||||||||

Purely syntactical conversions to propositional formulas | ||||||||||||||||||||||||||

iLIT :: ILit -> PropForm IAtom | ||||||||||||||||||||||||||

iNLC :: ILine -> PropForm IAtom | ||||||||||||||||||||||||||

iNLD :: ILine -> PropForm IAtom | ||||||||||||||||||||||||||

iCNF :: IForm -> PropForm IAtom | ||||||||||||||||||||||||||

iDNF :: IForm -> PropForm IAtom | ||||||||||||||||||||||||||

xLIT :: Ord a => XLit a -> PropForm a | ||||||||||||||||||||||||||

xNLC :: Ord a => XLine a -> PropForm a | ||||||||||||||||||||||||||

xNLD :: Ord a => XLine a -> PropForm a | ||||||||||||||||||||||||||

xCNF :: Ord a => XForm a -> PropForm a | ||||||||||||||||||||||||||

xDNF :: Ord a => XForm a -> PropForm a | ||||||||||||||||||||||||||

Conversions to and from propositional formulas | ||||||||||||||||||||||||||

toXPDNF :: Ord a => PropForm a -> XPDNF a | ||||||||||||||||||||||||||

toXPCNF :: Ord a => PropForm a -> XPCNF a | ||||||||||||||||||||||||||

toM2DNF :: Ord a => PropForm a -> MixForm a | ||||||||||||||||||||||||||

toM2CNF :: Ord a => PropForm a -> MixForm a | ||||||||||||||||||||||||||

fromXPDNF :: Ord a => XPDNF a -> PropForm a | ||||||||||||||||||||||||||

fromXPCNF :: Ord a => XPCNF a -> PropForm a | ||||||||||||||||||||||||||

fromMixForm :: Ord a => MixForm a -> PropForm a | ||||||||||||||||||||||||||

The IForm algebra | ||||||||||||||||||||||||||

Basic operations | ||||||||||||||||||||||||||

isIAtom :: Int -> Bool | ||||||||||||||||||||||||||

isILit :: Int -> Bool | ||||||||||||||||||||||||||

isILine :: Costack Int -> Bool | ||||||||||||||||||||||||||

isIForm :: Costack (Costack Int) -> Bool | ||||||||||||||||||||||||||

iLine :: [Int] -> ILine | ||||||||||||||||||||||||||

iForm :: [[Int]] -> IForm | ||||||||||||||||||||||||||

iAtom :: ILit -> IAtom | ||||||||||||||||||||||||||

iBool :: ILit -> Bool | ||||||||||||||||||||||||||

negLit :: ILit -> ILit | ||||||||||||||||||||||||||

lineIndices :: ILine -> Olist IAtom | ||||||||||||||||||||||||||

formIndices :: IForm -> Olist IAtom | ||||||||||||||||||||||||||

lineLength :: ILine -> Int | ||||||||||||||||||||||||||

formLength :: IForm -> Int | ||||||||||||||||||||||||||

volume :: IForm -> Int | ||||||||||||||||||||||||||

isOrderedForm :: IForm -> Bool | ||||||||||||||||||||||||||

orderForm :: IForm -> IForm | ||||||||||||||||||||||||||

The propositional algebra operations | ||||||||||||||||||||||||||

atomForm :: IAtom -> IForm | ||||||||||||||||||||||||||

botForm :: IForm | ||||||||||||||||||||||||||

topForm :: IForm | ||||||||||||||||||||||||||

formJoinForm :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

formListJoin :: [IForm] -> IForm | ||||||||||||||||||||||||||

lineMeetLine :: ILine -> ILine -> IForm | ||||||||||||||||||||||||||

lineMeetForm :: ILine -> IForm -> IForm | ||||||||||||||||||||||||||

formMeetForm :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

formListMeet :: [IForm] -> IForm | ||||||||||||||||||||||||||

dualLine :: ILine -> IForm | ||||||||||||||||||||||||||

dualForm :: IForm -> IForm | ||||||||||||||||||||||||||

invertLine :: ILine -> ILine | ||||||||||||||||||||||||||

invertForm :: IForm -> IForm | ||||||||||||||||||||||||||

negLine :: ILine -> IForm | ||||||||||||||||||||||||||

negForm :: IForm -> IForm | ||||||||||||||||||||||||||

formCojoinLine :: IForm -> ILine -> IForm | ||||||||||||||||||||||||||

formCojoinForm :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

formAntijoinLine :: IForm -> ILine -> IForm | ||||||||||||||||||||||||||

formAntijoinForm :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

elimLine :: ILine -> Olist IAtom -> ILine | ||||||||||||||||||||||||||

elimForm :: IForm -> Olist IAtom -> IForm | ||||||||||||||||||||||||||

lineCovLine :: ILine -> ILine -> Bool | ||||||||||||||||||||||||||

lineCovForm :: ILine -> IForm -> Bool | ||||||||||||||||||||||||||

formCovForm :: IForm -> IForm -> Bool | ||||||||||||||||||||||||||

Generation of pairwise minimal, minimal and prime forms | ||||||||||||||||||||||||||

Generation of prime and pairwise minimal forms of two lines | ||||||||||||||||||||||||||

pairPartition :: ILine -> ILine -> (ILine, ILine, ILine, ILine) | ||||||||||||||||||||||||||

data CaseSymbol | ||||||||||||||||||||||||||

| ||||||||||||||||||||||||||

caseSymbol :: ILine -> ILine -> CaseSymbol | ||||||||||||||||||||||||||

pairPrim' :: ILine -> ILine -> IForm | ||||||||||||||||||||||||||

pairMin' :: ILine -> ILine -> IForm | ||||||||||||||||||||||||||

xprim' :: ILine -> ILine -> (CaseSymbol, IForm) | ||||||||||||||||||||||||||

xmin' :: ILine -> ILine -> (CaseSymbol, IForm) | ||||||||||||||||||||||||||

xprim :: ILine -> ILine -> (CaseSymbol, IForm) | ||||||||||||||||||||||||||

xmin :: ILine -> ILine -> (CaseSymbol, IForm) | ||||||||||||||||||||||||||

pairPrim :: ILine -> ILine -> IForm | ||||||||||||||||||||||||||

pairMin :: ILine -> ILine -> IForm | ||||||||||||||||||||||||||

Implementation of the M- and the P-Procedure | ||||||||||||||||||||||||||

isMinimalPair :: ILine -> ILine -> Bool | ||||||||||||||||||||||||||

allPairs :: [a] -> [(a, a)] | ||||||||||||||||||||||||||

isPairwiseMinimal :: IForm -> Bool | ||||||||||||||||||||||||||

cPrime :: ILine -> ILine -> Maybe ILine | ||||||||||||||||||||||||||

cPrimes :: IForm -> IForm | ||||||||||||||||||||||||||

mrec :: (IForm, IForm, IForm) -> IForm | ||||||||||||||||||||||||||

m2form :: IForm -> IForm | ||||||||||||||||||||||||||

iformJoinM2form :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

primForm :: IForm -> IForm | ||||||||||||||||||||||||||

iformJoinPrimForm :: IForm -> IForm -> IForm | ||||||||||||||||||||||||||

The XForm operations | ||||||||||||||||||||||||||

xformAtoms :: Ord a => XForm a -> Olist a | ||||||||||||||||||||||||||

xformRedAtoms :: Ord a => XForm a -> Olist a | ||||||||||||||||||||||||||

xformIrrAtoms :: Ord a => XForm a -> Olist a | ||||||||||||||||||||||||||

The propositional algebras | ||||||||||||||||||||||||||

XPDNF and XPCNF | ||||||||||||||||||||||||||

MixForm | ||||||||||||||||||||||||||

mixToPDNF :: Ord a => MixForm a -> MixForm a | ||||||||||||||||||||||||||

mixToPCNF :: Ord a => MixForm a -> MixForm a | ||||||||||||||||||||||||||

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

Produced by Haddock version 2.4.2 |