PropLogic

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.

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

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

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

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 PropForm a, and the two-parameter type class PropAlg a p for the abstract notion of a propositional algebra. These two notions are described in more detail in the PropLogicCore module.

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.

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.

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.