FastPropLogic
 Contents Introductory example Generating a Prime Disjunctive Normal Form, the default and the fast way XPDNF as a propositional algebra The canonization steps Syntax Conversions IdxPropForm -- indexed propositional formulas Purely syntactical conversions to propositional formulas Conversions to and from propositional formulas The IForm algebra Basic operations The propositional algebra operations Generation of pairwise minimal, minimal and prime forms Generation of prime and pairwise minimal forms of two lines Implementation of the M- and the P-Procedure The XForm operations The propositional algebras XPDNF and XPCNF MixForm Complexities and choice of a algebra
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, 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.

Synopsis
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 = XPDNF (XForm a)
data XPCNF a = XPCNF (XForm a)
data MixForm a
 = M2DNF (XForm a) | M2CNF (XForm a) | PDNF (XForm a) | PCNF (XForm a)
type IdxPropForm a = (Olist a, PropForm IAtom)
tr :: (s -> t) -> PropForm s -> PropForm t
iTr :: Olist IAtom -> IForm -> IForm
idx :: Ord a => Olist a -> a -> IAtom
nth :: Ord a => Olist a -> IAtom -> a
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
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
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
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
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
pairPartition :: ILine -> ILine -> (ILine, ILine, ILine, ILine)
data CaseSymbol
 = NOOO | NOOP | NOPO | NOPP | NIOO | NIOP | NIPO | NIPP | NMNN
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
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
xformAtoms :: Ord a => XForm a -> Olist a
xformRedAtoms :: Ord a => XForm a -> Olist a
xformIrrAtoms :: Ord a => XForm a -> Olist a
mixToPDNF :: Ord a => MixForm a -> MixForm a
mixToPCNF :: Ord a => MixForm a -> MixForm a
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
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
Constructors
 XPDNF (XForm a) Instances
 Ord a => PropAlg a (XPDNF a) Eq a => Eq (XPDNF a) Read a => Read (XPDNF a) Show a => Show (XPDNF a) Display a => Display (XPDNF a)
data XPCNF a
Constructors
 XPCNF (XForm a) Instances
 Ord a => PropAlg a (XPCNF a) Eq a => Eq (XPCNF a) Read a => Read (XPCNF a) Show a => Show (XPCNF a) Display a => Display (XPCNF a)
data MixForm a
Constructors
 M2DNF (XForm a) M2CNF (XForm a) PDNF (XForm a) PCNF (XForm a) Instances
 Ord a => PropAlg a (MixForm a) Eq a => Eq (MixForm a) Read a => Read (MixForm a) Show a => Show (MixForm a) Display a => Display (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

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

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

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 :: 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
Constructors
 NOOO NOOP NOPO NOPP NIOO NIOP NIPO NIPP NMNN Instances
 Eq CaseSymbol Ord CaseSymbol Read CaseSymbol Show 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
.........
.........
```