Python Propositions

Author: Danny Yoo (dyoo@hkn.eecs.berkeley.edu)

Introduction
 
    This is a small package for propositional logic --- it provides a
    few tools for representing and playing around with propositional
    logic objects.  For now, it contains a parser to build AST trees
    out of most propositional phrases:

    ###
    >>> import parser
    >>> print parser.parse('jack and jill and bill or ted')
    or[and[and[jack, jill], bill], ted]
    ###

    as well as a silly algorithm for turning propositions into a set of
    states:

    ###
    >>> import algorithm
    >>> algorithm.getTrueStates(
    ...     parser.parse('2b or not 2b implies question'))
    [{'2b': 'T', 'question': 'T'}, {'2b': 'F', 'question': 'T'}]
    ###

    As you might guess, it's nowhere near done yet.  Still, it might
    be useful for someone, so I'm putting up my work up before I
    forget.  There are some transformation functions in algorithm.py,
    but I'm planning a big reorganization/renaming soon, since some of
    the functions aren't named "obviously" enough.


Supported parser grammar:

    We support the keywords:

        and, or, not, implies, equals.

    To make things more palatable for people who like symbolism, we
    also support:

        &&, ||, !, ->, =
    
    as well as parentheses to override precedence rules.

    I've used John Aycock's wonderful Spark parser generator, with a
    few homegrown changes to make it die less when it sees bad
    grammars.
    

Background:

    I started reading David Gries's "The Science of Programming", and
    got caught up in chapters 2 and 4.  Question 2.8 asked:

        """Show that any proposition e and be transformed into an
        equivalent proposition in \emph{conjunctive normal form} ---
        i.e. one that has the form

            e_0 and ... and e_n
                
            where each e_i has the form:

            g_0 and ... g_m

        Each g_j is an identifier ID, a unary operator (not ID), T, or
        F.  Furthermore the identifiers in each e_i are distinct."""

    I had trouble actually putting the proof into words, but I knew in
    my gut that I could write a program to do it for me.  That's how
    this whole mess started.  *grin*

    September 20, 2001: I'm happy to say that I've finally implemented
    my answer in algorithm.normalizeToConjunction().  I'm not quite
    sure if it's correct, but it looks like it works... *grin*


Todo:

    Make a graphical interface

        Allow selective evaluation of propositions, similar to what
        MacGambit Scheme provides with its Replacement Modeler.

    Implement more equivalence transformers

        De morgan, or-simplifcation, and-simplification, the works.
        I'll want to at least implement the 12 laws of propositional
        equivalence from David Gries "The Science of Programming".

    Make the code usable for other people

        I have not really been thinking of other people while writing
        this code.  *grin* I'll need to reorganize things to make them
        more obviously useful (or useless).

    Use PyUnit for testing / Follow documentation standards.

        I want a cool LaTeX-ified web page too!