FastPropLogic

Introductory example

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

XPDNF as a propositional algebra

The canonization steps

Syntax

type IAtom

type ILit

type ILine

type IForm

type XLit a

type XLine a

type XForm a

data XPDNF a

data XPCNF a

data MixForm a

Conversions

IdxPropForm -- indexed propositional formulas

type IdxPropForm a

tr

iTr

idx

nth

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

data 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