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

if there is no 1's, but only 0's.

For our example formula, this is

PropLogic> satisfiable phi
True
PropLogic> valid phi
False
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
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                 |
+---+---+----------------------------------+

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

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