Introduction to PropLogic
January 2010
Bucephalus.org

# Preliminaries

For the following interactive tutorial, we assume that the Glasgow Haskell Compiler suite [GHC] is installed, the interpreter `ghci` is running and `PropLogic` is loaded. The installation process is fully described in [Inst].

If all that has been done, the interpreter shows the

`  PropLogic>`

prompt or something similar. In the examples below, we use that to indicate that the text after the prompt is input, and the following line(s) are the according interpreter response. For example,

```  PropLogic> T `equivalent` F
False```

means that the input of `T `equivalent` F` returns the answer `False`.

# Core Concepts

## Propositional Formulas

A typical propositional formula in common mathematical notation is

¬(rain ∧ snow) &and (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬hot)

But we don't have these symbols available in Haskell, a different encoding of formulas is required. In our attempt to compromise with the mathematical notation as well as the syntactic preferences of Haskell, we introduce propositional formulas in two versions:

There is a "fancy" version, similar to the mathematical notation, with arithmetic symbols `*`, `+`, `-` for conjunctions, disjunctions and negation, respectively, and in which our example looks like

`  [-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]]`

And there is a "pure" version, which is the actual Haskell syntax, but less convenient for direct input,

```  CJ [N (CJ [A "rain", A "snow"]),
EJ [A "wet", DJ [A "rain", A "snow"]],
SJ [A "rain", A "hot"],
SJ [A "snow", N (A "hot")]]```

The following table shows the grammar of the two kinds of formulas:

Pure formulas `ProForm a` Fancy formulas `A α` `ω` atomic formula `F` `false` zero or false `T` `true` unit or true `N φ` `-φ` negation `CJ [φ1,...,φn]` `[φ1 * ... * φn]` conjunction `DJ [φ1,...,φn]` `[φ1 + ... + φn]` disjunction `SJ [φ1,...,φn]` `[φ1 -> ... -> φn]` subjunction `EJ [φ1,...,φn]` `[φ1 <-> ... <-> φn]` equijunction where
• `α` is an atom of the given atom type `a` (which is arbitrary, e.g. `String` or `Integer`, but consistent for all atoms)
• `ω` is a nonempty string of digits letter, but without any quotation marks around it, e.g. `hallo`, `007`, `omega13`
• `φ`, `φ1`, ..., `φn` are formulas.
Note, that the square brackets `[...]` around the `n`-ary junctions are mandatory in fancy formulas. (There are no preference rules, just plain syntax.)

The pure syntax is the real definition of propositional formulas in Haskell, which goes

```  data PropForm a         -- Propositional Formulas on Atom type a
= A a                 -- atomic formula
| F                   -- boolean false or zero value
| T                   -- boolean true or unit value
| N (PropForm a)      -- negation
| CJ [PropForm a]     -- conjunction
| DJ [PropForm a]     -- disjunction
| SJ [PropForm a]     -- subjunction
| EJ [PropForm a]     -- equijunction```

and these formulas can be treated as Haskell values (also with `read` and `show`).

Fancy formulas are no Haskell values at all, but we obtain them as output when we apply the `display` function on pure formulas, e.g.

```  PropLogic> display (EJ [A "rain", CJ [A "hot", A "wet"]])
[rain <-> [hot * wet]]```

or for an example of type `PropForm Integer` we obtain

```  PropLogic> display (N (EJ [A 1234, A 2345]))
-[1234 <-> 2345]```

On the other hand, we can wrap a fancy formula as a `String` inside double quotes `"..."` and parse this as a formula on string atoms with the function

`  stringToProp :: String -> PropForm String`

To demonstrate that on the two previous examples, we obtain

```  PropLogic> stringToProp "[rain <-> [hot * wet]]"
EJ [A "rain",CJ [A "hot",A "wet"]]```
```  PropLogic> stringToProp "-[1234 <-> 2345]"
N (EJ [A "1234",A "2345"])```

Note, that the last result is not of the original type `PropForm Integer`, but of type `PropForm String`.

As you will have noticed, conjunctions and disjunctions may have not just two, but any number of arguments. This is much more convenient for the definition of certain normal forms. Less common however is the use of `n`-ary subjunctions and equijunctions. The rules for their semantics are:

`[φ1 -> ... -> φn] ⇔ [[-φ1 + φ2] * ... * [-φn-1 + φn]]`
```[φ1 <-> ... <-> φn] ⇔ [[-φ1 * ... * -φn] + [φ1 * ... * φn]] ```

``` ```

``` Propositional Algebras The Truth-Table Semantics of Formulas Let us take a simple formula and call it phi. In a ghci session, we can set local definitions with a let-expression, say PropLogic> let phi = EJ [A 'x', CJ [A 'y', A 'z']] This is a formula of type PropForm Char and we can confirm its pure and fancy form with PropLogic> phi EJ [A 'x',CJ [A 'y',A 'z']] PropLogic> display phi [x <-> [y * z]] With the atoms function, we obtain the set of atoms {'x','y','z'} occurring in phi. Actually, the result is not a set, but the strictly ordered list ['x','y','z'], the type is Olist Char, where type Olist a = [a] is simply our type synonym for ordered list, which are used to represent finite sets. Recall, that the list of characters is written as a string in Haskell, so we actually obtain PropLogic> atoms phi "xyz" A semantics of propositional formulas is defined by its truth table. The idea is pretty standard and we can ask for the usual intuitive display of the truthTable of phi by calling PropLogic> display (truthTable phi) +---+---+---+-----------------+ | x | y | z | [x <-> [y * z]] | +---+---+---+-----------------+ | 0 | 0 | 0 | 1 | +---+---+---+-----------------+ | 0 | 0 | 1 | 1 | +---+---+---+-----------------+ | 0 | 1 | 0 | 1 | +---+---+---+-----------------+ | 0 | 1 | 1 | 0 | +---+---+---+-----------------+ | 1 | 0 | 0 | 0 | +---+---+---+-----------------+ | 1 | 0 | 1 | 0 | +---+---+---+-----------------+ | 1 | 1 | 0 | 0 | +---+---+---+-----------------+ | 1 | 1 | 1 | 1 | +---+---+---+-----------------+ The first of the eight (non-header) rows is saying that, if we valuate phi with the valuator that assigns false to each of the atoms, then the evaluation of this valuated formula is true. Actually, we can reconstruct this idea stepwise: A valuator is an ordered list of pairs, made of atoms and boolean values. In our case, the atoms are of type Char, thus the valuator is of type Valuator Char: PropLogic> let omega = [('x',False),('y',False),('z',False)] :: Valuator Char Recall our example formula PropLogic> phi EJ [A 'x',CJ [A 'y',A 'z']] the omega-valuation of phi is a nullatomic formula PropLogic> valuate omega phi EJ [F,CJ [F,F]] and a nullatomic formula can be evaluated to a boolean value, here: PropLogic> boolEval (valuate omega phi) True The combination of a valuation and an evaluation is an application and we can do that, too PropLogic> boolApply phi omega True These boolean versions of evaluation and application return Bool values, i.e. boolEval :: PropForm a -> Bool boolApply :: PropForm a -> Valuator a -> Bool There are also more general versions, returning formulas again, eval :: PropForm a -> PropForm a apply :: PropForm a -> Valuator a -> PropForm a (The actual types of all these definitions are a little more complex; but that is not important here. You can check a type of a value v with the :type or :t command, i.e. type :t v after the prompt and the interpreter returns its type. You can also ask the interpreter to return the type for every output with the command :set +t.) For the given three atoms 'x', 'y', 'z' there are 2^3 = 8 different valuators, and that are the eight rows of the displayed truth table. So, mathematically speaking, a truth table is a second-order boolean function (A -> Bool) -> Bool where A is the given atom set. Such a construction however is not possible in Haskell, we cannot turn an ordered list of atoms into a type. The idea remains the same, but the actual type definition is type TruthTable a = (Olist a, Maybe (PropForm a), [([Bool], Bool)]) (The first argument is the head row of the ordered atoms, the second argument is the optional formula that is repeated in the result column, and the third argument is a straight version of the rows, each one of type ([Bool],Bool).) The Semantic Structure on Formulas Truth tables provide us with a denotational semantics for formulas. But there are also the common semantic concepts that alltogether make a quasi-boolean structure. All these notions can be defined in terms of the truth tables. Recall, that a formula is called satisfiable if the result column of its truth table has at least one 1 valid if the result column of its truth table has only 1's and no 0 at all, and contradictory if there is no 1's, but only 0's. For our example formula, this is PropLogic> satisfiable phi True PropLogic> valid phi False PropLogic> contradictory phi False And there are the usual semantic comparison relations: Two formulas phi and psi are called equivalent if boolApply phi omega = boolApply psi omega, for every valuator omega subvalent if boolApply phi omega <= boolApply psi omega, for every valuator omega We can check that automatically with two functions of the same name. But recall the usual Haskell conventions on binary functions: instead of operating on pairs of formulas, like so equivalent (form1, form2) Haskell functions are usually currfied and called by equivalent form1 form2 with the option to place the function between the arguments when wrapped inside backticks form1 `equivalent` form2 For example PropLogic> (CJ [A 'x', A 'y']) `subvalent` (A 'x') True PropLogic> (SJ [A 'x', A 'y']) `equivalent` (DJ [N (A 'x'), A 'y']) True You can verify the last example by checking that the truth tables of the two formulas are equal. More conveniently, you can use the multiTruthTable function, that takes a list of formulas as input and displays them by one table with one result column for every formula. An example with three formulas is PropLogic> display (multiTruthTable [SJ [A 'x', A 'y'], DJ [N (A 'x'), A 'y'], N (CJ [A 'x', N (A 'y')])]) +--------------------------------+ | MultiTruthTable | | 1. [x -> y] | | 2. [-x + y] | | 3. -[x * -y] | | +---+---+------+------+------+ | | | x | y | 1. | 2. | 3. | | | +---+---+------+------+------+ | | | 0 | 0 | 1 | 1 | 1 | | | +---+---+------+------+------+ | | | 0 | 1 | 1 | 1 | 1 | | | +---+---+------+------+------+ | | | 1 | 0 | 0 | 0 | 0 | | | +---+---+------+------+------+ | | | 1 | 1 | 1 | 1 | 1 | | | +---+---+------+------+------+ | +--------------------------------+ The three result columns are identical, the formulas are pairwise equivalent, thus. The Algebra of Truth Tables Suppose, phi and psi are two formulas, and ttPhi and ttPsi are their truth tables, PropLogic> let ttPhi = truthTable phi PropLogic> let ttPsi = truthTable psi We just instruced a couple of semantic notions for formulas by looking and comparing their truth tables. But we may as well abstract from the form of formulas and consider their truth table semantics right away. In other words, we say that a truth table is satisfiable (valid, contradictory) if it has some (or only, or no) 1 in its result column. And we can apply the same functions on truth tables as well, e.g. PropLogic> satisfiable ttPhi Of course, we always have (satisfiable ttPhi) == (satisfiable phi) And similarly, we adopt the semantic relations for truth tables, and the rule is, that (ttPhi `subvalent` ttPsi) == (phi `subvalent` psi) Furthermore, we introduce the junctors on truth tables in the same fashion: there is a negation neg :: TruthTable a -> TruthTable a which, of course, negates the boolean values in the result column of each table. And there is the conjunction conj, the disjunction disj, the subjunction subj and the equijunction equij that operate in harmony with the formula constructors CJ, DJ, SJ, and EJ, respectively, in the sense that e.g. conj [ttPhi, ttPsi] `equivalent` truthTable (CJ [phi, psi]) Propositional Algebras For every atom type a, we now have a structure on PropForm a and a similar one on TruthTable a. We call such a structure a propositional algebra, the elements of a are the atoms, and the formulas or truth tables are the propositions. We define this abstract kind of structure as a type class in Haskell: PropAlg a p is the type class for a propositional algebra on atom type a and proposition type p. And we already have two instances of this type class for every atom type a, namely PropAlg a (PropForm a) PropAlg a (TruthTable a) The concept of a propositional algebra is the core concept of the whole package and the implementation of instances is the main achievement. Components of a Propositional Algebra A propositional algebra PropAlg a p on atoms a and propositions p comprises the following functions. Formula conversions Every instance of a propositional algebra has two functions to convert propositions to formulas, and backwards: toPropForm :: p -> PropForm a fromPropForm :: PropForm a -> p On the formula algebra PropAlg a (PropForm a), these two functions are obviously the identity functions. On the truth table algebra PropAlg a (TruthTable a), the fromPropForm is just another name for truthTable :: PropForm a -> TruthTable a Note however, that the use of fromPropForm requires a specification of the type. Haskell wouldn't know otherwise, to which kind of proposition we want to convert the formula. For example, a call of PropLogic> fromPropForm (EJ [A 'x', A 'y']) returns an error message, but PropLogic> fromPropForm (EJ [A 'x', A 'y']) :: TruthTable Char returns a TruthTable Char value. The inverse function toPropForm on the other hand is the same as truthTableToDNF :: TruthTable a -> PropForm a which turns a truth table into a Disjunctive Normal Form or DNF. For example, PropLogic> let tt = fromPropForm (EJ [A 'x', A 'y']) :: TruthTable Char PropLogic> display tt +---+---+-----------+ | x | y | [x <-> y] | +---+---+-----------+ | 0 | 0 | 1 | +---+---+-----------+ | 0 | 1 | 0 | +---+---+-----------+ | 1 | 0 | 0 | +---+---+-----------+ | 1 | 1 | 1 | +---+---+-----------+ PropLogic> let dnf = toPropForm tt PropLogic> display dnf [[-x * -y] + [x * y]] You are probably familiar with DNFs (see below). And, as you probably expected, there is also a dual function that returns the Conjunctive Normal Forms PropLogic> display (truthTableToCNF tt) [[x + -y] * [-x + y]] Semantic Functions Most of the semantic properties and relations were explained earlier, but there are also some variations: covalence means that the arguments have at least one valuator in common that makes them true, disvalence is the opposite of covalence, and proper disvalence means disvalence and both arguments are satisfiable. Alltogether, the signature is valid :: p -> Bool satisfiable :: p -> Bool contradictory :: p -> Bool subvalent :: p -> p -> Bool equivalent :: p -> p -> Bool covalent :: p -> p -> Bool disvalent :: p -> p -> Bool properSubvalent :: p -> p -> Bool properDisvalent :: p -> p -> Bool The set of junctors is false :: p true :: p neg :: p -> p conj :: [p] -> p disj :: [p] -> p subj :: [p] -> p equij :: [p] -> p On the formula algebra PropAlg a (PropForm a), these junctor are the formula constructors themselves false = F true = T neg = N conj = CJ disj = DJ subj = SJ equij = EJ On PropAlg a (TruthTable a), false and true are the two different nullatomic tables with either 0 or 1 in their result table. (Note, that there is one valuator for the empty atom set, namely the empty valuator [].) We also need an atomic proposition constructor at :: a -> p For formulas, this is again the atomic formula constructor at = A. The atomic truth table of say the atom 'x' is given by PropLogic> display (at 'x' :: TruthTable Char) +---+---+ | x | | +---+---+ | 0 | 0 | +---+---+ | 1 | 1 | +---+---+ Note, that we often need to type things for Haskell to indicate the instance we have in mind. For the previous example that means that an untyped call of say PropLogic> at 'x' would issue an error message, because it is not clear, if the result is of type PropForm Char or TruthTable Char or any other instance. Another algebraization of propositional logic The previous operations alltogether define what we call the semantic structure of a propositional algebra, and that is the most often used aspect of propositional logic. In fact, this semantic part has an abstract counterpart, called boolean algebra, and it is common to reduce propositional logic to this semantic aspect. (A standard method to do so is the Lindenbaum-Tarski algebra, see e.g. [LTA].) But our algebraization of propositional logic results in a kind of structure we call theory algebra. That is a specific combination of not just one, but two order structures, namely the semantic as well as the atomic (or syntactic) structure. (See [ThA].) The Atomic Structure First of all, there are three functions that return atom sets (i.e. ordered lists of atoms) atoms :: p -> Olist a redAtoms :: p -> Olist a irrAtoms :: p -> Olist a For example, if we put PropLogic> let phi = EJ [A "first", CJ [A "second", F], A "first"] PropLogic> display phi [first <-> [second * false] <-> first] then we already now that atoms returns the atoms (here: Strings), that occur in the formula: PropLogic> atoms phi ["first","second"] This atom set is further split into redundant and irredundant atoms: PropLogic> redAtoms phi ["second"] PropLogic> irrAtoms phi ["first"] An atom is redundant in a formula, if there is an equivalent formula without that atom. In this given phi, "second" is redundant and an equivalent formula psi is e.g. PropLogic> let psi = N (A "first") PropLogic> psi `equivalent` phi True Then, there is a whole variation of atomic properties and relations, nullatomic :: p -> Bool subatomic :: p -> p -> Bool equiatomic :: p -> p -> Bool coatomic :: p -> p -> Bool disatomic :: p -> p -> Bool properSubatomic :: p -> p -> Bool properDisatomic :: p -> p -> Bool As the names suggest, a proposition is nullatomic if it has not atoms. And if phi and psi are two propositions, then phi is subatomic to psi, i.e. PropLogic> phi `subatomic` psi True if each atom in phi is also an atom in psi. phi and psi are said to be coatomic, if they have at least one common atom. Otherwise, they are disatomic. And proper disatomic means that they are disatomic, and none of them is nullatomic. Atomic modifiers The junctions always accumulate the atoms of their arguments, just as the formulas did. The conjunction (or disjunction etc.) of propositions contains all the atoms of the given propositions together. But we have no operation so far, that decreases the number of atoms again. Therefore, we define a couple of atomic modifiers. Each modifier is of type p -> [a] -> p, i.e. it takes a proposition phi and a list of atoms [a1,...,aN] and it returns a new proposition psi, which should be equivalent to the intial one. The modifier is called a reduction, if psi has exactly the atoms [a1,...,aN]. It is an elimination if psi has the atoms from phi, but without the ones in [a1,...,aN]. And finally, it is an extension (or expansion), if the atoms of psi are the union of the ones in phi and [a1,...,aN]. The extension is the easiest of the modifications, because it always has a solution, i.e. for each phi and [a1,...,aN], there always is an equivalent psi with all the atoms of phi and [a1,...,aN]. An (atomic) extension (or expansion) takes a proposition and a list of atoms, and returns a proposition which is equivalent, but has these additional atoms. For formulas, this can be done in terms of formula constructors according to the rule ext phi [a1,...,aN] == CJ [phi, DJ [T, A a1, ..., A aN]] Note, that the right hand of the equation is indeed equivalent to phi. This is indeed the chosen implementation. For example, PropLogic> ext (A 'y') ['x', 'z'] CJ [A 'y',DJ [T,A 'x',A 'z']] Reductions and eliminations are more difficult, because they often don't have a solution. Suppose, phi is the formula CJ [A 'x', A 'y', A 'z'] and we want to perform a reduction onto the atoms 'x', 'y'. That is impossible, because there is no formula psi with atoms psi == ['x', 'y'] and psi `equivalent` phi. However, there always is a supremum (or least upper) and a infimum (or greatest lower) reduction. For example, the supremum reduction supRed phi [a1,...,aN] is the least of all formulas psi so that the a1,...,aN are the atoms of psi (with respect to the subvalence order relation). Similarly, there is a supremum elimination and a infimum elimination and alltogether, there are five atomic modifiers in a propositional algebra: ext :: p -> [a] -> p infRed :: p -> [a] -> p supRed :: p -> [a] -> p infElim :: p -> [a] -> p supElim :: p -> [a] -> p The implementation of these modifiers is usually not a trivial operation and we won't go into the details here. For example PropLogic> let ttPhi = truthTable (SJ [A 'x', A 'y', A 'z']) PropLogic> display ttPhi +---+---+---+---------------+ | x | y | z | [x -> y -> z] | +---+---+---+---------------+ | 0 | 0 | 0 | 1 | +---+---+---+---------------+ | 0 | 0 | 1 | 1 | +---+---+---+---------------+ | 0 | 1 | 0 | 0 | +---+---+---+---------------+ | 0 | 1 | 1 | 1 | +---+---+---+---------------+ | 1 | 0 | 0 | 0 | +---+---+---+---------------+ | 1 | 0 | 1 | 0 | +---+---+---+---------------+ | 1 | 1 | 0 | 0 | +---+---+---+---------------+ | 1 | 1 | 1 | 1 | +---+---+---+---------------+ PropLogic> display (supElim ttPhi ['y']) +---+---+----------------------------------+ | x | z | [[-x * -z] + [-x * z] + [x * z]] | +---+---+----------------------------------+ | 0 | 0 | 1 | +---+---+----------------------------------+ | 0 | 1 | 1 | +---+---+----------------------------------+ | 1 | 0 | 0 | +---+---+----------------------------------+ | 1 | 1 | 1 | +---+---+----------------------------------+ PropLogic> display (infElim ttPhi ['y']) +---+---+----------------------------------+ | x | z | [[x + z] * [-x + z] * [-x + -z]] | +---+---+----------------------------------+ | 0 | 0 | 0 | +---+---+----------------------------------+ | 0 | 1 | 1 | +---+---+----------------------------------+ | 1 | 0 | 0 | +---+---+----------------------------------+ | 1 | 1 | 0 | +---+---+----------------------------------+ Additional definitions Two propositions are called biequivalent, iff they are both equivalent and equiatomic. In terms of Haskell p1 `biequivalent` p2 == (p1 `equivalent` p2) && (p1 `equiatomic` p2) Biequivalence is the identity from a theory-algebraic point of view. The last two functions that make up a propositional algebra PropAlg a p are two "meta properties" that generalize semantic and atomic properties P and relations R for lists of propositions. We say that such a list [q_1,...,q_n] is pointwise P, if P q is True for every q in the list. And it is pairwise R, if q_i R q_j holds for all 1 <= i < j <= n. In Haskell these meta properties are functions pointwise :: (p -> Bool) -> [p] -> Bool pairwise :: (p -> p -> Bool) -> [p] -> Bool (Actually, pointwise is just a synonym for the Haskell built-in all.) For example, PropLogic> let pL = [A 'x', N (A 'y'), CJ [A 'x', A 'z']] PropLogic> :t pL pL :: [PropForm Char] PropLogic> pointwise satisfiable pL True PropLogic> pairwise disatomic pL False PropLogic> pairwise coatomic pL False Summary The overall signature of the PropAlg type class definition is given by class Ord a => PropAlg a p | p -> a where -- atomic proposition constructor at :: a -> p -- boolean junctors false :: p true :: p neg :: p -> p conj :: [p] -> p disj :: [p] -> p subj :: [p] -> p equij :: [p] -> p -- semantic properties and relations valid :: p -> Bool satisfiable :: p -> Bool contradictory :: p -> Bool subvalent :: p -> p -> Bool equivalent :: p -> p -> Bool covalent :: p -> p -> Bool disvalent :: p -> p -> Bool properSubvalent :: p -> p -> Bool properDisvalent :: p -> p -> Bool -- atom sets atoms :: p -> Olist a redAtoms :: p -> Olist a irrAtoms :: p -> Olist a -- atomic properties and relations nullatomic :: p -> Bool subatomic :: p -> p -> Bool equiatomic :: p -> p -> Bool coatomic :: p -> p -> Bool disatomic :: p -> p -> Bool properSubatomic :: p -> p -> Bool properDisatomic :: p -> p -> Bool -- atomic modifiers ext :: p -> [a] -> p infRed :: p -> [a] -> p supRed :: p -> [a] -> p infElim :: p -> [a] -> p supElim :: p -> [a] -> p -- biequivalence biequivalent :: p -> p -> Bool -- meta properties pointwise :: (p -> Bool) -> [p] -> Bool pairwise :: (p -> p -> Bool) -> [p] -> Bool -- formula conversions toPropForm :: p -> PropForm a fromPropForm :: PropForm a -> p Other Parts of the Package "Default" and "fast" instances and the modular character of the package In fact, there are more than just the two default instances on formulas and truth tables PropAlg a (PropForm a) PropAlg a (TruthTable a) We call them default, because their idea is straight forward and so is their implementation. But the problem with the default instances is that some representations and operations explode, and that makes them not feasible for other than small cases with only a few atoms involved. For example, a truth table on n atoms has 2^n valuators, and checking for subvalence the default way may be of exponential cost as well. Next to the default instances we therefore also provide a couple of fast propositional algebras as well, that aim to be feasible for arbitrary practical situations. This whole approach is also apparent in the modular design of the package. The four important modules are: PropLogicCore / \ / \ / \ DefaultPropLogic FastPropLogic \ / \ / \ / PropLogicTest PropLogicCore basically comprises the definition for the PropForm a data type and the PropAlg a p type class. DefaultPropLogic provides the default implementations we discussed so far, but also default implementations of various normalizations. FastPropLogic implements a couple of fast instances for propositional algebras and PropLogicTest provides generators for the various different proposition types, methods to check the correctness and performance of propositional algebra instances. All modules also come with built-in documentations (see [Doc]). Normalizations, Canonizations and the Fast Instances of Propositional Algebras ....sorry, this is work in progress.... The "fast" instances of Propositional Algebras ....sorry, this is work in progress.... Links and Footnotes [GHC] http://www.haskell.org/ghc points to the Glasgow Hakell Compiler. [Inst] http://www.bucephalus.org/text/InstallPropLogic/InstallPropLogic.html describes the installation of the various requirements. [LTA] http://en.wikipedia.org/wiki/Lindenbaum-Tarski_algebra the Wikipedia article on Lindenbaum-Tarski algebras. [ThA] http://www.bucephalus.org/text/TheoryAlgebras/TheoryAlgebras.html the guide to literature on Theory Algebras. [Doc] The Haskell modules all come with their own HTML documentation (see http://www.bucephalus.org/PropLogic). ```