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
.
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:
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.[...]
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}] * ... * [φ_{n1} + φ_{n}]]
[φ_{1} <> ... <> φ_{n}] ⇔ [[φ_{1} * ... * φ_{n}] + [φ_{1} * ... * φ_{n}]]
Propositional Algebras
The TruthTable 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 (nonheader) 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 secondorder 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 quasiboolean 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 LindenbaumTarski 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: String
s), 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 theoryalgebraic 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 builtin 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 builtin 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]

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/LindenbaumTarski_algebra
the Wikipedia article on LindenbaumTarski 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).