FastPropLogic

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.

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