PropLogic-0.9.0.1: A system for propositional logic with default and fast instances of propositional algebras.

DefaultPropLogic

Description

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.

Synopsis

# 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` 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)Source

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.

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

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

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

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.

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

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

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

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

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

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.

For example,

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

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

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

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

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)]
```

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)]
```

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

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

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

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

as explained above. In fact, `truthTableToDNF = valuatorListToDNF . truthTableUnitValuators`. Actually, the result is not only a `DNF`, but even a `NaturalDNF`, as described below.

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 `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 z, A x, A z, A y, A z]` is (bi-)equivalent to `CJ [A x, A y, A z]`.

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

is `True` iff the argument is an ordered propositional formula.

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

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

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.

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

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

returns the boolean value of a literal form, e.g.

``` > litFormValue (A 'x')
True
```
``` > litFormValue (N (A 'x'))
False
```

## Negation Normal Forms

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.

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

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.

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

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

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

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

checks if the formula is a NLD.

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

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

## 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 aSource

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

type PCNF a = CNF aSource

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

For example,

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

### 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 aSource

type MCNF a = CNF aSource

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