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.

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.

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

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.

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

This module comprises the abstract definition of two core concepts of propositional logic:

• The data type (PropForm a) of propositional formulas, based on a given atom type a.
• The two-parameter type class (PropAlg a p) of a propositional algebra, where a is the atom type and p the type of propositions. Operations of such a structure include a decision if two propositions are equivalent, if a given proposition is satisfiable, a converter toPropForm and the inverse fromPropForm, 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.

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

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 (:), (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.

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.

1. (PropAlg a (PropForm a)), is the standard propositional algebra, where the propositions are actually the propositional formulas.
2. (PropAlg a (TruthTable a)) is a less common, but nevertheless very intuitive propositional algebra, which is based on truth tables.
3. (PropAlg Void Bool) instantiates the predefined algebra Bool of 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 a of atoms. But the propositional algebra on Bool 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.

1. (PropAlg a (XPDNF 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.
2. (PropAlg a (XPCNF a)) is the dual version of the previous algebra, elements are indexed prime conjunctive normal forms.
3. (PropAlg a (MixForm 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.

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.