| |||||||
| |||||||
| |||||||
Description | |||||||
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. | |||||||
Synopsis | |||||||
| |||||||
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:
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.
(II) In the FastPropLogic module defines a small variety of propositional algebras where the propositions are certain kinds of normal forms.
| |||||||
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. | |||||||
Produced by Haddock version 2.4.2 |