- The composition and modules
- Propositional algebras
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 so-called Prime Normal Forms in particular.
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.
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 two-parameter type class
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
The composition and modules
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
<= and the boolean junctors
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
This module comprises the abstract definition of two core concepts of propositional logic:
- The data type
(of propositional formulas, based on a given atom type
- The two-parameter type class
(of a propositional algebra, where
ais the atom type and
pthe type of propositions. Operations of such a structure include a decision if two propositions are
equivalent, if a given proposition is
satisfiable, a converter
toPropFormand the inverse
fromPropForm, which turns a propositional formula into a proposition.
Propositional logic the default style and the descriptive introduction of (canonic) normalizations
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 non-traditional 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
Instances of propositional algebras with fast implementations
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.
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.
TextDisplay implements some methods for the two-dimensional 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
Olist has methods for treating ordered lists as finite sets.
Costack is the implementation of a concatenable stack, i.e. it re-defines the standard Haskell functions
(++). 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.
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 two-parameter type class
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.
(PropAlg a (is a less common, but nevertheless very intuitive propositional algebra, which is based on truth tables.
(PropAlginstantiates the predefined algebra
Boolof boolean values as a propositional algebra, the one with the empty atom type
Void. Actually, all other instances of propositional algebras are equally powerful in the sense that they can all be based on an arbitrary type
aof atoms. But the propositional algebra on
Boolis 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.
(PropAlg a (is the dual version of the previous algebra, elements are indexed prime conjunctive normal forms.
(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.
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 non-exponentiality 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.