 Syntactic operations
 Semantics
 Normal Forms
 Propositional algebras
This module implements the basic operations of propositional logic in a very default way, i.e. the definitions and implementations are very intuitive and the whole module can be seen as a reconstruction and tutorial of propositional logic itself. However, some of these implementations are not feasible for other than very small input, because the intuitive algorithms are sometimes too ineffective.
Next to some syntactical tools, we provide a common reconstruction of the semantics with an emphasis on truth tables.
As a result, we obtain two default models of a propositional algebra, namely
PropAlg a (PropForm a)
the propositional algebra on propositional formulas PropForm
and
PropAlg a (TruthTable a)
the algebra on the socalled truth tables TruthTable
(each one on a linearly ordered atom type a
).
Additionally, we also instantiate the predefined boolean value algebra on Bool
as a trivial, because atomless propositional algebra.
Another important concept is the normalization. We introduce a whole range of normalizers and canonizers of propositional formulas.
 juncDeg :: PropForm a > Int
 juncArgs :: PropForm a > [PropForm a]
 juncCons :: Int > [PropForm a] > PropForm a
 atomSize :: PropForm a > Int
 juncSize :: PropForm a > Int
 size :: PropForm a > Int
 type LiteralPair a = (a, Bool)
 type Valuator a = Olist (LiteralPair a)
 correctValuator :: Ord a => [LiteralPair a] > Valuator a
 valuate :: Ord a => Valuator a > PropForm a > PropForm a
 boolEval :: PropForm a > Bool
 boolApply :: Ord a => PropForm a > Valuator a > Bool
 allValuators :: Ord a => [a] > Olist (Valuator a)
 zeroValuators :: Ord a => PropForm a > Olist (Valuator a)
 unitValuators :: Ord a => PropForm a > Olist (Valuator a)
 type TruthTable a = (Olist a, Maybe (PropForm a), [([Bool], Bool)])
 correctTruthTable :: Ord a => ([a], Maybe (PropForm a), [([Bool], Bool)]) > TruthTable a
 truthTable :: Ord a => PropForm a > TruthTable a
 plainTruthTable :: Ord a => PropForm a > TruthTable a
 truthTableBy :: Ord a => PropForm a > [a] > (Valuator a > Bool) > TruthTable a
 type MultiTruthTable a = (Olist a, [PropForm a], [([Bool], [Bool])])
 correctMultiTruthTable :: Ord a => ([a], [PropForm a], [([Bool], [Bool])]) > MultiTruthTable a
 multiTruthTable :: Ord a => [PropForm a] > MultiTruthTable a
 valuatorToNLC :: Valuator a > NLC a
 valuatorToNLD :: Valuator a > NLD a
 valuatorListToCNF :: [Valuator a] > CNF a
 valuatorListToDNF :: [Valuator a] > DNF a
 nlcToValuator :: NLC a > Valuator a
 nldToValuator :: NLD a > Valuator a
 cnfToValuatorList :: CNF a > [Valuator a]
 dnfToValuatorList :: DNF a > [Valuator a]
 truthTableZeroValuators :: TruthTable a > [Valuator a]
 truthTableUnitValuators :: TruthTable a > [Valuator a]
 truthTableToDNF :: TruthTable a > NaturalDNF a
 truthTableToCNF :: TruthTable a > NaturalCNF a
 type OrdPropForm a = PropForm a
 isOrdPropForm :: Ord a => PropForm a > Bool
 ordPropForm :: Ord a => PropForm a > OrdPropForm a
 type EvalNF a = PropForm a
 isEvalNF :: PropForm a > Bool
 eval :: PropForm a > EvalNF a
 apply :: Ord a => PropForm a > Valuator a > EvalNF a
 type LitForm a = PropForm a
 isLitForm :: PropForm a > Bool
 litFormAtom :: LitForm a > a
 litFormValue :: LitForm a > Bool
 type NegNormForm a = PropForm a
 isNegNormForm :: PropForm a > Bool
 negNormForm :: PropForm a > NegNormForm a
 type NLC a = NegNormForm a
 isNLC :: Ord a => PropForm a > Bool
 type NLD a = NegNormForm a
 isNLD :: Ord a => PropForm a > Bool
 type CNF a = NegNormForm a
 isCNF :: Ord a => PropForm a > Bool
 type DNF a = NegNormForm a
 isDNF :: Ord a => PropForm a > Bool
 type NaturalDNF a = DNF a
 type NaturalCNF a = CNF a
 isNaturalDNF :: Ord a => PropForm a > Bool
 isNaturalCNF :: Ord a => PropForm a > Bool
 naturalDNF :: Ord a => PropForm a > NaturalDNF a
 naturalCNF :: Ord a => PropForm a > NaturalCNF a
 type PDNF a = DNF a
 type PCNF a = CNF a
 primeDNF :: Ord a => PropForm a > PDNF a
 primeCNF :: Ord a => PropForm a > PCNF a
 validates :: Ord a => Valuator a > PropForm a > Bool
 falsifies :: Ord a => Valuator a > PropForm a > Bool
 directSubvaluators :: Valuator a > [Valuator a]
 allDirectSubvalidators :: Ord a => Valuator a > PropForm a > [Valuator a]
 allDirectSubfalsifiers :: Ord a => Valuator a > PropForm a > [Valuator a]
 primeValuators :: Ord a => PropForm a > [Valuator a]
 coprimeValuators :: Ord a => PropForm a > [Valuator a]
 type MDNF a = DNF a
 type MCNF a = CNF a
 minimalDNFs :: Ord a => PropForm a > [MDNF a]
 minimalCNFs :: Ord a => PropForm a > [MCNF a]
 type SimpleDNF a = PropForm a
 type SimpleCNF a = PropForm a
 simpleDNF :: Ord a => DNF a > SimpleDNF a
 simpleCNF :: Ord a => CNF a > SimpleCNF a
 ext' :: PropForm a > Olist a > PropForm a
Syntactic operations
Formula Deconstructors
returns a junctor degree 0,1,...,,7
, in case the formulas is created with A,F,T,N,CJ,DJ,SJ,EJ
, respectively.
For example,
> juncDeg (A 'x') 0 > juncDeg (CJ [A 'x', F]) 4
returns the list of arguments of the outer junctor of the given formula, e.g.
> juncArgs (SJ [A 'x', F, CJ [A 'y', T]]) [A 'x',F,CJ [A 'y',T]] > juncArgs F [] > juncArgs (N T) [T] > juncArgs (A 'x') [A 'x']
is the junction constructor, which is defined so that for every formula p
holds
juncCons (juncDeg p) (juncArgs p) == p
For example,
> juncCons 5 [juncCons 0 [A 'x'], juncCons 1 [], juncCons 3 [juncCons 2 []]] DJ [A 'x',F,N T]
Size
counts the number of atoms (including multiple occurrences), i.e. each occurrence of an A
.
atomSize ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 4
counts the number of bit values and junctions, i.e. each occurrence of F
, T
, N
, CJ
, DJ
, SJ
, EJ
juncSize ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 5
The overall size of a formula, where
(size f) = (atomSize f) + (juncSize f)
For example
size ( CJ [DJ [A "x", N (A "y")], DJ [A "x", A "z"], T] ) == 9
Linear syntactic order on formulas
.....................................CONTINUEHERE ....................................................
Semantics
A denotational semantics for propositional formulas is defined by the basic idea, that the truth table of a formula
defines its meaning. Formally speaking, if A = {a1, ..., aN}
is the atom set of a given formula φ, then each valuator,
i.e. each function ω :: A > Bool
turns φ into an either True
or False
value (namely boolApply φ ω
).
The summary of these 2^N
valuatorvalue pairs is formalized by a function (A > Bool) > Bool
, and that is what we call
the truth table of φ (namely truthTable φ
).
For example, if φ is a ↔ b
, then the atom set is {a,b}
. And if tt = truthTable φ
, then we can
display tt
and obtain
++++  a  b   ++++  0  0  1  ++++  0  1  0  ++++  1  0  0  ++++  1  1  1  ++++
Implementing this idea in Haskell is not that straight forward however, because Haskell doesn't allow type constructions like
(atoms φ) > Bool
for valuators and ((atoms φ) > Bool) > Bool
for truth tables. So we need to make some adaptions.
Valuators and formulas as functions
type LiteralPair a = (a, Bool)Source
type Valuator a = Olist (LiteralPair a)Source
Ideally, a valuator is a finite function {a1,...,aN} > Bool
and we can represent it as a list of atomvalue pairs
[(a1,b1),...,(aN,bN)]
. We disambiguate and increase the efficiency of this representation, when we demand that a1 < ... < aN
,
according to a given order on the atoms. But declaring Valuator a
as Olist (a, Bool)
only makes (a1, b1) < ... < (aN, bN)
.
For example, [(
is a x
,False),(x
,True)]Valuator Char
, but obviously not a correct one, as we call it.
correctValuator :: Ord a => [LiteralPair a] > Valuator aSource
If the given list of literal pairs makes a correct valuator, then this argument is returned as it is. Otherwise, an error occurs. For example,
> correctValuator [('x', False), ('y', True)] [('x',False),('y',True)] > correctValuator [('x', False), ('x', True)] *** Exception: correctValuator: multiple occurring atoms > correctValuator [('y', False), ('x', True)] *** Exception: correctValuator: atoms are not in order
valuate ω φ
takes the formula φ and replaces its atoms by boolean values according to ω. For example,
> valuate [('x', True), ('y', False)] (EJ [A 'x', N (A 'x'), A 'y', A 'z', A 'y']) EJ [T,N T,F,A 'z',F]
boolEval ω
evaluates a nullatomic formula ω to a boolean value according to the common semantics for the
junctions N
, DJ
, ..., but causes an error when ω is not nullatomic. For example,
> boolEval (DJ [T, F]) True > boolEval (CJ [T, F]) False > boolEval (EJ [T,T]) True > boolEval (CJ [T, SJ [F, F]]) True > boolEval (CJ [T, A 'x'])  error ...
(Note, that we also provide a generalization eval
of boolEval
below.)
combines valuate
and boolEval
, i.e.
boolApply p v = boolEval (valuate v p)
For example,
> boolApply (EJ [A 'x', A 'y']) [('x', True), ('y', True)] True > boolApply (EJ [A 'x', A 'y']) [('x', True), ('y', False)] False > boolApply (EJ [A 'x', A 'y']) [('x', True)]  error
(Note, that we also provide a generalization apply
of boolApply
below.)
allValuators :: Ord a => [a] > Olist (Valuator a)Source
For example
> allValuators ['y', 'x'] [[('x',False),('y',False)],[('x',False),('y',True)],[('x',True),('y',False)],[('x',True),('y',True)]]
zeroValuators φ
returns all valuators ω
(on the atom set of φ
) with boolApply φ ω = False
.
For example,
> zeroValuators (CJ [A 'x', A 'y']) [[('x',False),('y',False)],[('x',False),('y',True)],[('x',True),('y',False)]]
unitValuators φ
returns all valuators ω
(on the atom set of φ
) with boolApply φ ω = Truee
.
For example,
> unitValuators (CJ [A 'x', A 'y']) [[('x',True),('y',True)]]
Truth tables
A truth table is thus a triple (atomList, optForm, tableBody)
, where atomList
is the ordered list of atoms, optForm
is
the optional formula that is a representation for this table, and tableBody
holds the rows of the table.
For example, if the table tt :: TruthTable String
is display
ed by
++++  x  y   ++++  0  0  1  ++++  0  1  0  ++++  1  0  0  ++++  1  1  1  ++++
then tt
has the formal representation as
(["x","y"],Nothing,[([False,False],True),([False,True],False),([True,False],False),([True,True],True)])
The optional formula Maybe (PropForm String)
is Nothing
in this case, and this makes it a plain table.
But it is common and often convenient to write the formula that represents this table in the head row as well.
Such a truth table is e.g. given by
(["x","y"],Just (EJ [A "x",A "y"]),[([False,False],True),([False,True],False),([True,False],False),([True,True],True)])
And when we display
it, we obtain
++++  x  y  [x <> y]  ++++  0  0  1  ++++  0  1  0  ++++  1  0  0  ++++  1  1  1  ++++
correctTruthTable :: Ord a => ([a], Maybe (PropForm a), [([Bool], Bool)]) > TruthTable aSource
checks if the given argument makes indeed a proper truth table. If so, the argument is returned unaltered. Otherwise, an according error message is returned.
truthTable :: Ord a => PropForm a > TruthTable aSource
returns the truth table of the given formula, with the formula itself included in the header. For example,
> truthTable (EJ [A "abc", F]) (["abc"],Just (EJ [A "abc",F]),[([False],True),([True],False)]) > display it +++  abc  [abc <> false]  +++  0  1  +++  1  0  +++
plainTruthTable :: Ord a => PropForm a > TruthTable aSource
as truthTable
, but this time without the formula included. For the same example, this is
> plainTruthTable (EJ [A "abc", F]) (["abc"],Nothing,[([False],True),([True],False)]) > display it +++  abc   +++  0  1  +++  1  0  +++
truthTableBy :: Ord a => PropForm a > [a] > (Valuator a > Bool) > TruthTable aSource
By default, the truth table of a formula φ, i.e. the right result column of the table is constructed with
boolApply φ ω
for the valuator ω
in each of the rows. Now truthTableBy
is a generalization of this
construction and allows other functions of type Valuator a > Bool
for this process, as well.
Multiple truth tables
It is common and efficient, for example when comparing several formulas for equivalence, to write these formulas in just
one table and add a result row for each formula. For example, the two formulas ¬(x → y)
and x ∧ ¬ y
are equivalent and we can verify that by comparing the two result columns in their tables. We call
> multiTruthTable [N (SJ [A 'x', A 'y']), CJ [A 'x', N (A 'y')]] ("xy",[N (SJ [A 'x',A 'y']),CJ [A 'x',N (A 'y')]], [([False,False],[False,False]),([False,True],[False,False]),([True,False],[True,True]),([True,True],[False,False])]) > display it ++  MultiTruthTable   1. [x > y]   2. [x * y]   +++++    x  y  1.  2.    +++++    0  0  0  0    +++++    0  1  0  0    +++++    1  0  1  1    +++++    1  1  0  0    +++++  ++
Similar to the type definition of TruthTable
as a triple (atoms, formulaList, tableBody)
.
correctMultiTruthTable :: Ord a => ([a], [PropForm a], [([Bool], [Bool])]) > MultiTruthTable aSource
returns the argument unchanged, if this is a wellformed MultiTruthTable
(with correct number of rows and columns etc.),
and returns an error, otherwise.
multiTruthTable :: Ord a => [PropForm a] > MultiTruthTable aSource
returns the common MultiTruthTable
of a formula list, where the atom list is the union of the atoms of all the formulas.
Mutual converters between syntax and semantics
With truthTable
we turned a PropForm
into a TruthTable
. But we can also turn a TruthTable
into a PropForm
.
However, this process is not unique anymore, because there are (infinitely) many formulas to represent each truth table.
Nevertheless, there are two standard ways to do so:
 Each row with a result 1 (i.e. each unit valuator) is turned into a Normal Literal Conjunction or
NLC
and the disjunction of them is a Disjunctive Normal Form orDNF
, which represents the table.  Each row with a result 0 (i.e. each zero valuator) is turned into a Normal Literal Disjunction or
NLD
and the conjunction of them is a Conjunctive Normal Form orCNF
, which represents the table, too.
For example, if the TruthTable
is say
> let tt = truthTable (EJ [A 'x', A 'y']) > > display tt ++++  x  y  [x <> y]  ++++  0  0  1  ++++  0  1  0  ++++  1  0  0  ++++  1  1  1  ++++
then
> display (truthTableToDNF tt) [[x * y] + [x * y]] > display (truthTableToCNF tt) [[x + y] * [x + y]]
The following functions provides the whole range of transformations for valuators, valuator lists, truth tables, and the according normal forms.
valuatorToNLC :: Valuator a > NLC aSource
For example,
> valuatorToNLC [('x', True), ('y', False), ('z', True)] CJ [A 'x',N (A 'y'),A 'z']
valuatorToNLD :: Valuator a > NLD aSource
For example,
> valuatorToNLD [('x', True), ('y', False), ('z', True)] DJ [N (A 'x'),A 'y',N (A 'z')]
Note, that the literal values appear inverted, e.g. (
becomes x
, True)N (A
.
x
)
valuatorListToCNF :: [Valuator a] > CNF aSource
turns each valuator of the given list into its NLD
and returns their overall conjunction.
valuatorListToDNF :: [Valuator a] > DNF aSource
turns each valuator of the given list into its NLC
and returns their overall disjunction.
nlcToValuator :: NLC a > Valuator aSource
Inverse operation of valuatorToNLC
. Undefined, if the argument is not a NLC
.
For example
> nlcToValuator (CJ [A 'x', N (A 'y')]) [('x',True),('y',False)]
nldToValuator :: NLD a > Valuator aSource
Inverse operation of valuatorToNLD
. Undefined, if the argument is not a NLD
.
For example
> nldToValuator (DJ [A 'x', N (A 'y')]) [('x',False),('y',True)]
cnfToValuatorList :: CNF a > [Valuator a]Source
Inverse operation of valuatorListToCNF
, undefined if the argument is not a CNF
.
dnfToValuatorList :: DNF a > [Valuator a]Source
Inverse operation of valuatorListToDNF
, undefined if the argument is not a DNF
.
truthTableZeroValuators :: TruthTable a > [Valuator a]Source
extracts all valuators that have a 1
(i.e. True
) in their result column.
truthTableUnitValuators :: TruthTable a > [Valuator a]Source
extracts all valuators that have a 0
(i.e. False
) in their result column.
truthTableToDNF :: TruthTable a > NaturalDNF aSource
as explained above. In fact, truthTableToDNF = valuatorListToDNF . truthTableUnitValuators
.
Actually, the result is not only a DNF
, but even a NaturalDNF
, as described below.
truthTableToCNF :: TruthTable a > NaturalCNF aSource
the dual version of truthTableToDNF
. Again, the result is even a NaturalCNF
.
Normal Forms
Normalizations and Canonizations in general
Definition
Let S
be any type (or set) and ~
an equivalence relation on S
. A function nf :: S > S
is then said to be
 a normalizer for
~
, whenx ~ y
iff(nf x) ~ (nf y)
, for allx, y :: S
.  a canonic normalizer or canonizer for
~
, if it is a normalizer andx ~ y
implies(nf x) == (nf y)
, for allx, y :: S
.
If the normalizer is not a trivial one (like id :: S > S
), then the images (nf x)
for x :: S
alltogether are a proper
subset of S
itself, called normal forms. And they are canonic normal forms, if they are the result of a
canonizer, i.e. if no two different normal forms are equivalent.
Normalizations in Propositional Algebras
In a propositional algebra
we have three equivalence relations on the type PropAlg
a pp
of propositions:

equivalent
, the semantic equivalence relation 
equiatomic
, the equiatomic or atomic equivalence relation 
biequivalent
, the biequivalence or theoryalgebraic equivalence relation
Accordingly, we call a normalizer (or canonizer) nf :: p > p
a
 semantic normalizer, if it is a normalizer for
equivalent
,  atomic normalizer, if it is a normalizer for
equiatomic
 theoryalgebraic normalizer or binormalizer, if it is a normalizer for
biequivalent
Traditionally, a normalizer is always a semantic normalizer, and all the normalizers we further introduce in this module are
of this kind. The notion of an atomic normalizer is actually quite superfluous, because it is not really relevant in practice.
But in our concept of a propositional algebra PropAlg
, two propositions are considered equal (from this abstract point of view),
if they are biequivalent, i.e. if they are equivalent and also have the same atoms.
Default semantic normalizations
In this default approach to normalizations, we only introduce important and more or less common examples and don't built propositional algebras on them. Most of the normalizers are semantic normalizer.
We also hope to increase the understanding by introducing the normalizer not as a function nf :: PropForm a > PropForm a
,
but as nf :: PropForm a > NF a
, where type NF a = PropForm a
stands for the normal subset of formulas.
Ordered Propositional Formulas
Next to the semantic and atomic order relations, given by subvalent
and subatomic
, respectively, there is
also a formal order <=
defined on formulas.
Different to the semantic and atomic order, this formal order is not only a partial, but even a linear order relation.
In Haskell, these linear order structures are realized as instances of the Ord
type class, i.e. we can compare
formulas and check for <
, <=
, ==
between formulas etc, given that the atom type itself is ordered.
The actual implementation of the formal order is irrelevant here.
The only thing of importance here is that fact that we can use it and that way we can remove ambiguities and
increase the effectiveness of some operations. In other words, it induces a normalization as follows.
(Note however, that we did not simply use deriving
to implement it, because we adopted the common definition
of literals LitForm
, and that would have compromised an understanding of NLC
s and NLD
s as ordered formulas.
For example, we need N (A 10) < A 20
to be true.)
Recall from the axioms of propositional algebras, that conjunctions and disjunctions are both idempotent and commutative,
i.e. we can remove multiple occurring components and arbitrarily change the component order in each conjunction and
disjunction. The result is still (bi) equivalent.
For example, CJ [A
is (bi)equivalent to z
, A x
, A z
, A y
, A z
]CJ [A
.
x
, A y
, A z
]
type OrdPropForm a = PropForm aSource
A propositional formula φ
is said to be ordered, if the components φ1, φ2..., φN
of every
conjunction CJ [φ1, φ2..., φN]
and every disjunction DJ [φ1, φ2..., φN]
occurring in
φ
are strictly ordered in the sense that φ1 < φ2 < ... < φN
.
isOrdPropForm :: Ord a => PropForm a > BoolSource
is True
iff the argument is an ordered propositional formula.
ordPropForm :: Ord a => PropForm a > OrdPropForm aSource
turns each formula into a (bi)equivalent ordered form. For example,
> ordPropForm (DJ [A 'x', A 'x', A 'z', A 'y', A 'x']) DJ [A 'x',A 'y',A 'z']
> ordPropForm (CJ [A 'x', T, N (A 'x'), T, F, A 'x']) CJ [A 'x',F,T,N (A 'x')]  because A 'x' < F < T < N (A 'x')
Evaluated Normal Forms
It is common to avoid unary conjunctions CJ [φ]
and disjunctions DJ [φ]
, both are (bi)equivalent to φ
itself. And a nullary CJ []
is usually replaced by T
, and DJ []
by F
.
Nullary and unary sub and equijunctions are less common, but they are also easily replaceable by their equivalent form T
.
Another easy simplification of formulas is the involvement of F
or T
as subformulas. For example, N F
is obviously
(bi)equivalent to T
, CJ [φ, T, ψ]
is (bi)equivalent to CJ [φ, ψ]
and CJ [φ, F, ψ]
is equivalent to T
. Similar rules hold for the other junctions (although a little more complicated in case of SJ
and EJ
).
The replacement of these mentioned subformulas is quite an easy and effective (semantic) normalization and we call it
evaluation eval
, because it is in a certain way a generalization of the boolean evaluation boolEval
.
A formula is called an Evaluated Normal Form iff it is either F
or T
or a formula that neither has bit values
nor trivial junctions.
By having bit values we mean that it contains F
s or T
s as subformulas.
By having trivial junctions we mean nullary or unary junctions with CJ
, DJ
, SJ
, or EJ
as subformulas.
checks, if the given formula is indeed an Evaluated Normal Form. For example,
> isEvalNF ( T ) True > isEvalNF ( CJ [T, A 'x'] ) False  because the formula has a bit value T > isEvalNF ( CJ [] ) False  because the formula has a trivial junction, namely the nullary conjunction > isEvalNF ( SJ [A 'x'] ) False  because it has a trivial junction, namely an unary subjunction > isEvalNF ( CJ [A 'x', N (A 'y)] ) True  has neither bit values nor trivial junctions
Generalized evaluation and application for formulas: eval
and apply
eval
takes a given formula and returns an equivalent Evaluated Normal Form.
This way, it is a generalization of boolEval
, which was only defined for nullatomic formulas.
More precisely, if φ
is a nullatomic formula, then boolEval φ
is True
(or False
) iff bool φ
is
T
(or F
, respectively).
For example
> eval (N F) T > eval (DJ [A 'x', F, A 'y']) DJ [A 'x',A 'y'] > eval (DJ [A 'x', T, A 'y']) T > eval (EJ [A 'x', T]) A 'x' > eval (EJ [A 'x', F]) N (A 'x') > eval (EJ [A 'x', A 'y']) EJ [A 'x',A 'y']
eval
is not as powerful as e.g. valid
, i.e. it does not return T
for every valid input formula. For example,
> eval (DJ [A 'x', N (A 'x')]) DJ [A 'x', N (A 'x')]
The advantage is that eval
is only of linear time complexity (at least if the input formula does not contain subjunctions
or equijunctions; in which case the effort is somewhat greater).
Because the resulting formula is always equivalent to the argument formula, eval
is an example of a (semantic) normalizer
(see EvalNF
below).
As eval
is a generalization of boolEval
, apply
is a generalization of boolApply
, defined by
apply φ ω = eval (valuate ω φ)
.
For example,
> apply (DJ [A 'x', A 'y', A 'z']) [('y', True)] T
> apply (DJ [A 'x', A 'y', A 'z']) [('y', False)] DJ [A 'x',A 'z']
Literal Form(ula)s
A literal is an atom with an assigned boolean value. The type for the semantic version of a literal was earlier introduced
as the LiteralPair
. The formal version is the literal formula LitForm
, which is either an atomic formula A x
or a
negated atomic formula N (A x)
.
This is the common definition of a literal in logic, although more close to the original idea would be the form EJ [A x, T]
instead of A x
and EJ [A x, F]
instead of N (A x)
. But it is common in the literature to use the
shorter and (bi)equivalent versions A x
and N (A x)
, instead.
Of course, the literal formulas do not induce a normalization, most formulas don't have an equivalent literal formula. But literal formulas are important building blocks of the most important normalizations in propositional logic.
is the type synonym for all formulas A x
or N (A x)
.
checks if a formula is indeed a literal form.
litFormAtom :: LitForm a > aSource
returns the atom of a literal form, e.g.
> litFormAtom (A 'x') 'x'
> litFormAtom (N (A 'x')) 'x'
litFormValue :: LitForm a > BoolSource
returns the boolean value of a literal form, e.g.
> litFormValue (A 'x') True
> litFormValue (N (A 'x')) False
Negation Normal Forms
type NegNormForm a = PropForm aSource
A Negation Normal Form is either a literal form, or a conjunction or a disjunction of negation normal forms. This subset of propositional formulas is a normal subset in the sense that each formula has a (bi)equivalent negation normal form.
isNegNormForm :: PropForm a > BoolSource
checks if a given propositional formula is in negation normal form.
negNormForm :: PropForm a > NegNormForm aSource
is the according normalizer, i.e. it returns an equivalent negation normal form. For example,
> negNormForm (N (CJ [N (SJ [A 'x', A 'y']), N T, F])) DJ [CJ [DJ [N (A 'x'),A 'y']],CJ [],CJ []] > negNormForm (N (CJ [N (DJ [A 'x']), N (DJ [N (A 'x')])])) DJ [DJ [A 'x'],DJ [N (A 'x')]]
This conversion is based on four laws for the removal of T
, F
, SJ
and EJ
:
T ⇔ CJ[]
F ⇔ DJ[]
[φ1 → φ2 → ... → φN] ⇔ [[φ1 + φ2] * [φ2 + φ3] * ...]
[φ1 ↔ φ2 ↔ ... ↔ φN] ⇔ [[φ1 * φ2 * ... * φN] + [φ1 * φ2 * ... * φN]]
and seven laws to remove negations other than negations of atomic formulas:
T ⇔ DJ[]
F ⇔ CJ[]
φ ⇔ φ
[φ1 * φ2 * ... * φN] ⇔ [φ1 + φ2 + ... + φN]
[φ1 + φ2 + ... + φN] ⇔ [φ1 * φ2 * ... * φN]
[φ1 → φ2 → ... → φN] ⇔ [[φ1 * φ2] + [φ2 * φ3] + ...]
[φ1 ↔ φ2 ↔ ... ↔ φN] ⇔ [[φ1 + φ2 + ... + φN] * [φ1 + φ2 + ... + φN]]
Note, that each each formula does have an biequivalent negation normal form, but our normalizer only returns equivalent forms in general. For example,
> negNormForm (SJ [A 'x']) CJ []  i.e. the atom 'x' is lost and this result is only equivalent
NLCs and NLDs, CNFs and DNFs
Probably the most important and best known normal forms are the Conjunctive Normal Forms or CNFs and the Disjunctive Normal Forms or DNFs. These forms are mutually dual, as it is called.
Let us consider DNFs. Usually, a DNF is defined as a disjunction of conjunctions of literals. An example DNF would then be
DJ [CJ [A 'x', A 'y'], CJ [N (A 'y'), A 'y'], CJ [A 'z', N (A 'x')]]
But our definition of a DNF is more restrictive, because we demand each literal conjunction CJ [λ_1, ..., λ_n]
to be a normal literal conjunction in the sense that the literal atoms must be strictly ordered, i.e.
.
And this is obviously not the case for the second and third of the three literal conjunctions of the given example.
litFormAtom
λ_1 < ... < litFormAtom
λ_n
Every literal conjunction can easily be converted into a NLC, unless it contains a complementary pair of literal, such as the
CJ [N (A
. In that case, it is equivalent to y
), A y
]F
, and as a component of the disjunction, it may be removed
alltogether without changing the semantics.
So the example formula in a proper DNF version would be
DJ [CJ [A 'x', A 'y'], CJ [A 'x', N (A 'z')]]
Note, that NLCs, NLDs, DNFs and CNFs are further specializations of Negation Normal Forms, so it is intuitive to introduce them
as subtypes via the type
synonym.
type NLC a = NegNormForm aSource
A normal literal conjunction or NLC is a conjunction CJ [λ_1, ..., λ_n]
with
λ_1,...,λ_n ::
and LitForm
a
.
litFormAtom
λ_1 < ... < litFormAtom
λ_n
checks if the formula is indeed a NLC. For example,
> isNLC (CJ [A 'a', N (A 'b'), A 'c']) True
type NLD a = NegNormForm aSource
A normal literal disjunction or NLD is a disjunction DJ [λ_1, ..., λ_n]
with
λ_1,...,λ_n ::
and LitForm
a
.
litFormAtom
λ_1 < ... < litFormAtom
λ_n
checks if the formula is a NLD.
type CNF a = NegNormForm aSource
A Conjunctive Normal Form or CNF is a conjunction CJ [δ_1,...,δ_n]
, of NLDs δ_1,...,δ_n
.
checks if the argument is a CNF. For example,
> isCNF (CJ [DJ [A 'x', A 'y'], DJ [N (A 'x'), A 'z']]) True
type DNF a = NegNormForm aSource
A Disjunctive Normal Form or DNF is a disjunction DJ [γ_1,...,γ_n]
of NLCs γ_1,...,γ_n
.
checks if the argument is a DNF.
Natural DNFs and CNFs
Recall, that truthTable
takes a formula and returns a TruthTable
, and that we can use truthTableToDNF
to convert
this into a formula, again. Combining the two steps truthTableToDNF.truthTable
defines a normalization of formulas into
DNFs we call this the natural DNF of the formula.
Actually, it is more common to call this the canonic DNF, but this title is not correct in a strict understanding of
our canonizer notion.
For example, the two formulas DJ [A
and x
, T]DJ [A
are equivalent, but their natural DNFs are different, so
y
, T]naturalDNF
is not a semantic canonizer.
By the way, iIt is not an atomic canonizer either, because e.g. DJ [A
and its natural DNF x
, F]DJ[]
don't have
the same atoms.
A formal characterization of all the result DNFs of naturalDNF
says that: a DNF
is a NaturalDNF
iff all its component
NLCs are of the same length (i.e. they have the same atom set).
type NaturalDNF a = DNF aSource
type NaturalCNF a = CNF aSource
isNaturalDNF :: Ord a => PropForm a > BoolSource
isNaturalCNF :: Ord a => PropForm a > BoolSource
naturalDNF :: Ord a => PropForm a > NaturalDNF aSource
naturalCNF :: Ord a => PropForm a > NaturalCNF aSource
Prime DNFs and CNFs
Natural DNFs are not really efficient to use, except for trivial cases, because a formula of n
atoms comprises up to
2^n
NLCs, each one containing n
literals.
In an attempt to define shorter and more efficient versions of DNFs and CNFs, we come up with two different approaches:
one is the prime, the other one is the minimal normal form. The properties of these forms are very important for
our whole design. Some of them might be surprising, e.g. that prime and minimal forms are only sometimes identical, and
that prime forms do make (semantic) canonizations and minimal forms do not.
We first define and generate these prime forms here, minimal forms are introduced further below.
Formal definition
Prime Disjunctive Normal Forms
Given an arbitrary PropForm
φ
, a DNF
Δ = DJ [γ_1,...,γ_n]
and any NLC
γ = CJ [λ_1,...,λ_k]
, all on the same atom type. We say that

γ
is a factor ofΔ
, ifγ ⇒ Δ
, i.e. if&916;
. (Note, that each of the componentsγ_1,...,γ_n
ofΔ
is a factor ofΔ
.) 
γ
is a prime factor ofΔ
, if it is a factor and there is not different factorγ'
ofΔ
such thatγ ⇒ γ' ⇒ Δ
. In other words, we cannot delete any of the literalsλ_1,...,λ_k
inγ
without violating the subvalenceγ ⇒ Δ
. 
Δ
is a Prime Disjunctive Normal Form or PDNF, if theγ_1,...,γ_n
are exactly all the prime factors ofΔ
. To futher remove disambiguities, we also demand thatΔ
is ordered, as earlier defined, which means thatγ_1 < ... < γ_n
. 
Δ
is the (ordered) PDNF ofφ
iffΔ
is an (ordered) PDNF equivalent toΔ
.
It is easy to proof that every formula Δ
has one and only one equivalent PDNF.
So this does induce a semantic canonization of propositional formulas.
The canonization is not a bicanonization, however, because the normal form is not always equiatomic.
For example, DJ [CJ []]
is the PDNF of EJ [A 5, A 5]
, but the atom 5
is lost.
Prime Conjunctive Normal Forms
This is dual to the previous definition, i.e. given a formula φ
, a CNF
Γ = [δ_1,...,δ_n]
and
a NLD
δ = DJ [λ_1,...,λ_k]
, then

δ
is a cofactor ofΓ
, ifΓ ⇒ δ
. 
δ
is a prime cofactor ofΓ
, if it is a cofactor and we cannot delete any of the literalsλ_1,...,λ_k
inδ
without violating the subvalenceΓ ⇒ δ
. 
Γ
is a Prime Conjunctive Normal Form or PCNF, if theδ_1,...,δ
are exactly the set of all its prime cofactors, and if these cofactors are ordered. 
Γ
is the (ordered) PCNF ofφ
iffΓ
is an (ordered) PCNF equivalent toΔ
.
Again, each formula has a unique equivalent PCNF.
The Haskell types and functions
is the type synonym for Prime Disjunctive Normal Forms or PDNFs.
is the type synonym for Prime Conjunctive Normal Forms or PCNFs.
is the PDNF canonizer, i.e. it turns each given formula into its unique PDNF. For example,
> primeDNF (EJ [A 'x', A 'y']) DJ [CJ [N (A 'x'),N (A 'y')],CJ [A 'x',A 'y']] > display it  "it" is the previous value in a ghci session, here the PDNF [[x * y] + [x * y]] > primeDNF T DJ [CJ []]  all valid/tautological formulas have this same PDNF
> primeDNF F DJ []  all contradictory formulas have this same PDNF
is the PCNF canonizer, i.e. the result is the unique PCNF of the given formula. For example,
> primeCNF (EJ [A 'x', A 'y']) CJ [DJ [N (A 'x'),A 'y'],DJ [A 'x',N (A 'y')]] > display it  means: display the previous formulas [[x + y] * [x + y]] > primeCNF (EJ [A 'x', A 'x']) CJ []  which is the same PCNF for all tautological formulas
The default and the fast generation of Prime Normal Forms
We say that a valuator v
validates a formula p
, iff the p
application on v
is valid. In other words,
(validates v p) == valid (apply p v)
We say that a valuator v
falsifies a formula p
, iff the p
application on v
is unsatisfiable. In other words,
(falsifies v p) == not (satisfiable (apply p v))
directSubvaluators :: Valuator a > [Valuator a]Source
For example,
directSubvaluators [(2,True),(4,False),(6,True)] == [[(2,True),(4,False)],[(2,True),(6,True)],[(4,False),(6,True)]]
primeValuators :: Ord a => PropForm a > [Valuator a]Source
coprimeValuators :: Ord a => PropForm a > [Valuator a]Source
Reference to the fast generation of Prime Normal Forms
Note, that the PropLogic package also provides functions pdnf
and pcnf
that do exactly the same as primeDNF
and
primeCNF
.
.... CONTINUEHERE .....
Minimal DNFs and CNFs
minimalDNFs :: Ord a => PropForm a > [MDNF a]Source
minimalCNFs :: Ord a => PropForm a > [MCNF a]Source
Simplified DNFs and CNFs
Propositional algebras
..... CONTINUEHERE .....
PropAlg a (PropForm a)
, the Propositional Formula Algebra
..... CONTINUEHERE .....
PropAlg a (PropForm a)
, the Truth Table Algebra
..... CONTINUEHERE .....
PropAlg Void Bool
, the Boolean Value Algebra
Recall, that the boolean or bit value algebra is a predefined, integrated of Haskell, comprising:
False, True :: Bool not :: Bool > Bool (&&), (), (<), (<=), (==), (/=), (=>), (>) :: Bool > Bool > Bool and, or :: [Bool] > Bool compare :: Bool > Bool > Ordering,  where data Ordering = LT  EQ  GT all, any :: (a > Bool) > [a] > Bool
..... CONTINUEHERE .....