A powerful system for propositional logic. Defines an abstract concept of a propositional algebra and provides both default and fast instances. Emphasizes the use of (canonic) normalizations in general and socalled Prime Normal Forms in particular.
http://www.bucephalus.org/PropLogic/
is the homepage with additional information for a variety of users, including short and thorough introductions to the use of PropLogic and the mathematical background of the whole design.
 module PropLogicCore
 module DefaultPropLogic
 module FastPropLogic
 module PropLogicTest
Start
The whole package is very modular in itself, according to the different perspectives we take to approach the subject (as explained below). It is possible to be more specific in an application and to import only certain parts. But the easiest and recommended way is the import of just this PropLogic module, which is just the summary of its main parts.
This package uses certain extensions to the Haskell 98 standard.
In particular, the propositional algebra concept is implemented as a twoparameter type class PropAlg
.
The package is developed with GHC (the Glasgow Haskell Compiler) and that works fine.
Hugs works fine as well, but it requires to be started with hugs 98
.
The composition and modules
Introduction
Propositional logic (also called sentential logic) is a very standard and relatively uncomplicated system in itself.
The (binary) boolean value algebra is one of the simplest structures at all and a standard in almost every programming language.
(Recall, that it is in Haskell given by the type Bool
, made of True
and False
, the
order <=
and the boolean junctors not
, &&
and 
.)
A propositional algebra is then essentially defined as the extension of this boolean value algebra with free variables,
commonly called atoms.
But however dense an abstract characterization of a propositional algebra may be, most traditional introductions are more complex and start with a syntax, i.e. some choice of what propositional formulas should cover, a more or less diverse semantics, together with some calculus for semantically sound and complete manipulation of formulas.
The four main modules
In this Haskell version of propositional logic, one design principle is the separation of the different aspects in four main modules.
PropLogicCore / \ / \ / \ / \ DefaultPropLogic FastPropLogic \ / \ / \ / \ / PropLogicTest
The abstract core concepts
module PropLogicCore
This module comprises the abstract definition of two core concepts of propositional logic:
 The data type
(
of propositional formulas, based on a given atom typePropForm
a)a
.  The twoparameter type class
(
of a propositional algebra, wherePropAlg
a p)a
is the atom type andp
the type of propositions. Operations of such a structure include a decision if two propositions areequivalent
, if a given proposition issatisfiable
, a convertertoPropForm
and the inversefromPropForm
, which turns a propositional formula into a proposition.
PropLogicCore provides the interface for the toolbox most users would need in most real circumstances.
The actual PropAlg
instances are implemented in the following two modules.
Propositional logic the default style and the descriptive introduction of (canonic) normalizations
module DefaultPropLogic
DefaultPropLogic on the other hand provides one (actually more than one) instance of PropAlg
, along with a whole range of
additional functionalities. For example, it introduces the concepts of valuators and a truth tables.
The title default indicates the very straight forward, intuitive, and naive approach.
For example, the implementation for the satisfiability
function applies the naive test, if the truth table has at least one true in the result column.
In fact, in DefaultPropLogic, the semantics of propositional algebra is thoroughly reconstructed and that makes this
module suitable as an interactive tutorial for propositional logic itself and all the concepts of the abstract level.
(There is an according introduction available online.)
The DefaultPropLogic introduces something else, namely a nontraditional idea of what the standard operations are.
We don't bother with the introduction of a certain rule system or calculus and we don't reconstruct propositional logic as
a proof system.
Our approach is based on (canonic) normalizations instead.
In particular, we use special kinds of DNFs and CNFs (disjunctive or conjunctive normal forms), namely
prime normal forms, and all traditional problems come down to a single normalization.
For example, a formula φ is satisfiable iff the prime DNF is not the empty disjunction,
i.e. iff the call of primeDNF φ
returns another result than (∨)
.
All traditional problems can be solved with one single canonization such as primeDNF
or primeCNF
, respectively.
Instances of propositional algebras with fast implementations
module FastPropLogic
Prime Normal Forms are indeed distinguished and reasonably compact semantic canonizations of propositional formulas.
However, for all cases with more than just a trivial amount of atoms involved, the default implementations are not feasible,
because of the exponential cost explosing of these default methods.
In FastPropLogic we provide a complete new implementation, based on a fast system of algorithms.
Main goal is the construction of fast instances of the PropAlg
type class.
Additional functions
module PropLogicTest
The independent implementations of the default and the fast approach allows us to use one as a test for the other, because they should produce the same results. To do that systematically, PropLogicTest has random formula generators and test for correctness. Another goal is the investigation of the actual performance of the fast methods. Finally, this module contains some useful functions which use functions from both DefaultPropLogic and FastPropLogic.
Hidden modules
TextDisplay implements some methods for the twodimensional treatment of plain text output. This is a useful tool, for
example for the display of truth tables in interpreter sessions. It provides the display
function which can be applied to
all the main concepts (formulas, truth tables, normal forms), for more intuitive and graphical layout than calling print
.
Olist has methods for treating ordered lists as finite sets.
Costack is the implementation of a concatenable stack, i.e. it redefines the standard Haskell functions
(:)
, (null)
, head
, tail
, and (++)
. The concatenation (++)
is not a primitive function in Haskell, and a costack
is a data structure, where all these functions are primitive.
The Costack module is only used in the implementations of the FastPropLogic functions.
Propositional algebras
As mentioned already, the two core concepts in the implementation of our version of propositional logic are
propositional formulas, given as the data type
, and the twoparameter type class PropForm
a
for the abstract notion of a propositional algebra.
These two notions are described in more detail in the PropLogicCore module.
PropAlg
a p
The different instances
The actual implementation of PropAlg
instances is done in two other modules and in two different ways:
(I) In the DefaultPropLogic module, we implement three different propositional algebras in a standard, intuitive and straight forward way.

(PropAlg a (
, is the standard propositional algebra, where the propositions are actually the propositional formulas.PropForm
a)) 
(PropAlg a (
is a less common, but nevertheless very intuitive propositional algebra, which is based on truth tables.TruthTable
a)) 
(PropAlg
instantiates the predefined algebraVoid
Bool
)Bool
of boolean values as a propositional algebra, the one with the empty atom typeVoid
. Actually, all other instances of propositional algebras are equally powerful in the sense that they can all be based on an arbitrary typea
of atoms. But the propositional algebra onBool
is just the trivial algebra with the empty atom type and we neglect it in the comparison of the different instances below.
(II) In the FastPropLogic module defines a small variety of propositional algebras where the propositions are certain kinds of normal forms.

(PropAlg a (
is the algebra, where each proposition is an indexed prime disjunctive normal form. One distinctive feature of these forms is that they are canonic in the sense that two propositions are equivalent if and only if they are equal.XPDNF
a)) 
(PropAlg a (
is the dual version of the previous algebra, elements are indexed prime conjunctive normal forms.XPCNF
a)) 
(PropAlg a (
is a variation and mix of the previous two algebras. The normal forms here may be either conjunctive or disjunctive normal forms, they are not necessarily prime normal forms, but may only be pairwise minimal. So in this algebra, the propositions are no longer canonic. But the advantage is that all the junctions, i.e. the boolean operations such as negation, conjunction etc. are of polynomial complexity. And in applications, where predominanty junctions are used, this implementation of a propositional algebra is faster than the previous two.MixForm
a))
Feasibility and performance of the fast implementations
The default instances of PropAlg
(i.e. on formulas and truth tables) are not feasible for other than small problems, and
that is why we implemented some fast instances as well.
One example for a cost explosing is the call of satisfiable
applied to a formula φ. If φ has say n
different atoms,
then there are 2^n
different valuations of these atoms and in the worst case, we need to test for all these valuations, if
they make φ true or false. Not feasible means exponential in the worst input cases.
Not all functions of the algebra on formulas are not feasible in this sense.
But compare to the default instances, the fast instances are called fast, because none of their functions is exponential.
In fact, we cannot claim really, that this is actually true. We don't have a proof for the nonexponentiality of the fast functions. The only criterion for the feasibility of our implementations is empirical. For more detail and empirical data about the performance of the involved functions, we refer to the home page.