bucephalus.org

The `PropLogic` Haskell package

January 2010

Abstract

PropLogic is a Haskell package for propositional (i.e. sentential) logic.

The most important concept is the propositional algebra, introduced as an abstract theory (Haskell type class).
Different models (Haskell instances) of these propositional algebras are implemented: "default" as well as "fast" ones.
As the universal method for this approach, single normalizers and canonizers, in particular the Prime Normal Form canonizations, each replace all indeterministic methods of the traditional propositional calculus.

Version

The PropLogic package is published as version 0.9 (for "almost the first version") and its stability is labeled "experimental", because some non-essential features in the source code and gaps in the documentation are awaiting a final touch and upload. (These missing parts are identified with a red comment below.) With a little bit of luck however, none of these gaps affects the use or functionality of the package.

Docs

Installing the PropLogic package [InstallPropLogic.html]: Various ways to obtain and use the package.
A little program for propositional logic [ExecPropLogic.html]: The first part describes the use of the executable program, which enables some important functions to be used from the command line. This is a demonstration on how all classical problems of propositional logic can be solved with just one of those Prime Normal Form canonizations. The last part comprises a performance study on the actual speed of these functions. This is an introduction that requires no prior knowledge of Haskell.
Introduction to PropLogic [IntroToPropLogic.html]: The main concept of the PropLogic package is that of a propositional algebra, implemented as a Haskell type class, with various "default" and "fast" instances. This is an introduction to the basic design and functionality of the package, aiming at Haskell programmers. (The last part currently still has some unfinished pieces.)
PropLogic manual: Introduces propositional algebras and other concepts from a mathematical point of view. (This text is in progress and not published, yet.)
Theory and implementation of efficient canonical systems for sentential calculus, based on Prime Normal Forms [PNFCanon.html]: A paper (36 pages) with the mathematical foundation for the algorithms.

Built-in documents

The package comprises a couple of modules, each one in a separate Haskell (hs) file, and each one comes with its own document file (html), generated from the source code (with Haddock).

In particular, the DefaultPropLogic.html document in the list below is written so that it can also be used as an interactive introduction into propositional logic itself.

HTML file	Source code	Description
PropLogic.html	PropLogic.hs	summary of the whole package and its modules
PropLogicCore.html (needs a makeover)	PropLogicCore.hs	abstract definition of "propositional formula" and "propositional algebra"
DefaultPropLogic.html (some little pieces are still under construction)	DefaultPropLogic.hs	reconstruction of propositional logic, constructive introduction of normalizations and canonizations, and default instances of propositional algebras
FastPropLogic.html (not in a proper state, yet)	FastPropLogic.hs	more efficient instances of propositional algebras
PropLogicTest.html (not in a proper state, yet)	PropLogicTest.hs (the general test for propositional algebras is not fully implemented, yet)	random generators, tests and some other functions
Olist.html	Olist.hs	ordered lists and set-like operations on them
Costack.html	Costack.hs (Costacks are still implemented as Haskell lists.)	Haskell data structure for "concatenable stacks", i.e. lists, where concatenation is a trivial operation
TextDisplay.html	TextDisplay.hs	auxiliary module for plain text in two dimensions
Main.html	Main.hs	for the generation of the stand-alone program

Bugs and comments

Needless to say that comments are very appreciated. Please use the blog entry as the place for all discussion.

Remarks

There is also a Java applet (bucanon) that provides a similar functionality as the executable in the Haskell package, but has a graphical user interface. Its syntax for propositional formulas (BucanonSyntax.pdf) is similar to the "fancy" Haskell notation and it also comes with a series of documents (BucanonGuide.html).

The PropLogic Haskell package