DefaultPropLogic

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

Syntactic operations

Formula Deconstructors

juncDeg :: PropForm a -> Int

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

juncArgs :: PropForm a -> [PropForm a]

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']

juncCons :: Int -> [PropForm a] -> PropForm a

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

atomSize :: PropForm a -> Int

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

juncSize :: PropForm a -> Int

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

size :: PropForm a -> Int

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 valuator-value 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)

type Valuator a = Olist (LiteralPair a)

Ideally, a valuator is a finite function {a1,...,aN} -> Bool and we can represent it as a list of atom-value 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, [(x,False),(x,True)] is a Valuator Char, but obviously not a correct one, as we call it.

correctValuator :: Ord a => [LiteralPair a] -> Valuator a

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 :: Ord a => Valuator a -> PropForm a -> PropForm a

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 :: PropForm a -> Bool

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

boolApply :: Ord a => PropForm a -> Valuator a -> Bool

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)

For example

 > allValuators ['y', 'x']
 [[('x',False),('y',False)],[('x',False),('y',True)],[('x',True),('y',False)],[('x',True),('y',True)]]

zeroValuators :: Ord a => PropForm a -> Olist (Valuator a)

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 :: Ord a => PropForm a -> Olist (Valuator a)

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

type TruthTable a = (Olist a, Maybe (PropForm a), [([Bool], Bool)])

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 displayed 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 a

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 a

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 a

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 a

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

type MultiTruthTable a = (Olist a, [PropForm a], [([Bool], [Bool])])

Similar to the type definition of TruthTable as a triple (atoms, formulaList, tableBody).

correctMultiTruthTable :: Ord a => ([a], [PropForm a], [([Bool], [Bool])]) -> MultiTruthTable a

returns the argument unchanged, if this is a well-formed MultiTruthTable (with correct number of rows and columns etc.), and returns an error, otherwise.

multiTruthTable :: Ord a => [PropForm a] -> MultiTruthTable a

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:

1. 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 or DNF, which represents the table.
2. 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 or CNF, 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 a

For example,

 > valuatorToNLC [('x', True), ('y', False), ('z', True)]
 CJ [A 'x',N (A 'y'),A 'z']

valuatorToNLD :: Valuator a -> NLD a

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. (x, True) becomes N (A x).

valuatorListToCNF :: [Valuator a] -> CNF a

turns each valuator of the given list into its NLD and returns their overall conjunction.

valuatorListToDNF :: [Valuator a] -> DNF a

turns each valuator of the given list into its NLC and returns their overall disjunction.

nlcToValuator :: NLC a -> Valuator a

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 a

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]

Inverse operation of valuatorListToCNF, undefined if the argument is not a CNF.

dnfToValuatorList :: DNF a -> [Valuator a]

Inverse operation of valuatorListToDNF, undefined if the argument is not a DNF.

truthTableZeroValuators :: TruthTable a -> [Valuator a]

extracts all valuators that have a 1 (i.e. True) in their result column.

truthTableUnitValuators :: TruthTable a -> [Valuator a]

extracts all valuators that have a 0 (i.e. False) in their result column.

truthTableToDNF :: TruthTable a -> NaturalDNF a

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 a

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 ~, when x ~ y iff (nf x) ~ (nf y), for all x, y :: S.
• a canonic normalizer or canonizer for ~, if it is a normalizer and x ~ y implies (nf x) == (nf y), for all x, 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 PropAlg a p we have three equivalence relations on the type p of propositions:

• equivalent, the semantic equivalence relation
• equiatomic, the equiatomic or atomic equivalence relation
• biequivalent, the biequivalence or theory-algebraic 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
• theory-algebraic normalizer or bi-normalizer, 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 NLCs and NLDs 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 z, A x, A z, A y, A z] is (bi-)equivalent to CJ [A x, A y, A z].

type OrdPropForm a = PropForm a

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

is True iff the argument is an ordered propositional formula.

ordPropForm :: Ord a => PropForm a -> OrdPropForm a

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.

type EvalNF a = PropForm a

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 Fs or Ts as subformulas. By having trivial junctions we mean nullary or unary junctions with CJ, DJ, SJ, or EJ as subformulas.

isEvalNF :: PropForm a -> Bool

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 :: PropForm a -> EvalNF a

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

apply :: Ord a => PropForm a -> Valuator a -> EvalNF a

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.

type LitForm a = PropForm a

is the type synonym for all formulas A x or N (A x).

isLitForm :: PropForm a -> Bool

checks if a formula is indeed a literal form.

litFormAtom :: LitForm a -> a

returns the atom of a literal form, e.g.

 > litFormAtom (A 'x')
 'x'

 > litFormAtom (N (A 'x'))
 'x'

litFormValue :: LitForm a -> Bool

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 a

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

checks if a given propositional formula is in negation normal form.

negNormForm :: PropForm a -> NegNormForm a

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. litFormAtom λ_1 < ... < litFormAtom λ_n. And this is obviously not the case for the second and third of the three literal conjunctions of the given example.

Every literal conjunction can easily be converted into a NLC, unless it contains a complementary pair of literal, such as the CJ [N (A y), A y]. In that case, it is equivalent to 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 a

A normal literal conjunction or NLC is a conjunction CJ [λ_1, ..., λ_n] with λ_1,...,λ_n :: LitForm a and litFormAtom λ_1 < ... < litFormAtom λ_n.

isNLC :: Ord a => PropForm a -> Bool

checks if the formula is indeed a NLC. For example,

 > isNLC (CJ [A 'a', N (A 'b'), A 'c'])
 True

type NLD a = NegNormForm a

A normal literal disjunction or NLD is a disjunction DJ [λ_1, ..., λ_n] with λ_1,...,λ_n :: LitForm a and litFormAtom λ_1 < ... < litFormAtom λ_n.

isNLD :: Ord a => PropForm a -> Bool

checks if the formula is a NLD.

type CNF a = NegNormForm a

A Conjunctive Normal Form or CNF is a conjunction CJ [δ_1,...,δ_n], of NLDs δ_1,...,δ_n.

isCNF :: Ord a => PropForm a -> Bool

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 a

A Disjunctive Normal Form or DNF is a disjunction DJ [γ_1,...,γ_n] of NLCs γ_1,...,γ_n.

isDNF :: Ord a => PropForm a -> Bool

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 x, T] and DJ [A y, T] are equivalent, but their natural DNFs are different, so naturalDNF is not a semantic canonizer. By the way, iIt is not an atomic canonizer either, because e.g. DJ [A x, F] and its natural DNF 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 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

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

1. γ is a factor of Δ, if γ ⇒ Δ, i.e. if &916;. (Note, that each of the components γ_1,...,γ_n of Δ is a factor of Δ.)
2. γ 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 γ ⇒ Δ.
3. Δ 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.
4. Δ 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 bi-canonization, 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,...,&#955_k], then

1. δ is a cofactor of Γ, if Γ ⇒ δ.
2. δ 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 Γ ⇒ δ.
3. Γ 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.
4. Γ 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

type PDNF a = DNF a

is the type synonym for Prime Disjunctive Normal Forms or PDNFs.

type PCNF a = CNF a

is the type synonym for Prime Conjunctive Normal Forms or PCNFs.

primeDNF :: Ord a => PropForm a -> PDNF a

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

primeCNF :: Ord a => PropForm a -> PCNF a

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

validates :: Ord a => Valuator a -> PropForm a -> Bool

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)

falsifies :: Ord a => Valuator a -> PropForm a -> Bool

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]

For example,

 directSubvaluators [(2,True),(4,False),(6,True)] ==
  [[(2,True),(4,False)],[(2,True),(6,True)],[(4,False),(6,True)]]

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]

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

type MDNF a = DNF a

type MCNF a = CNF a

minimalDNFs :: Ord a => PropForm a -> [MDNF a]

minimalCNFs :: Ord a => PropForm a -> [MCNF a]

Simplified DNFs and CNFs

type SimpleDNF a = PropForm a

type SimpleCNF a = PropForm a

simpleDNF :: Ord a => DNF a -> SimpleDNF a

simpleCNF :: Ord a => CNF a -> SimpleCNF a

Propositional algebras

..... CONTINUEHERE .....

PropAlg a (PropForm a), the Propositional Formula Algebra

..... CONTINUEHERE .....

ext' :: PropForm a -> Olist a -> PropForm a

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