Date:         Mon, 28 Mar 2005 14:26:07 -0500
From: "William J. Rapaport" <rapaport@cse.Buffalo.EDU>
Subject: CSE 4/563:  PROJECT 1 UPDATE
To: CSE563-SP05-LIST@LISTSERV.BUFFALO.EDU

------------------------------------------------------------------------
Subject: CSE 4/563:  PROJECT 1 UPDATE
------------------------------------------------------------------------

As announced in lecture today, I am hereby extending the due date for
Project 1 to:

        Friday, April 15

(and I will modify the project webpages to reflect this)

In class, I also suggested the following strategies for handling this
project.  These are suggestions only!  If you are well on the way to
completing the project without taking these suggestions into account,
keep on with what you're doing!

1.  Treat the project as consisting of separable modules:

        a)  the clause-form algorithm

                *  this one you should be able to do now

        b)  the unification algorithm

                *  you can hold off on writing this until
                   we finish covering it in class (unless
                   you're reading ahead in the text :-)

        c)  a resolution applier that takes 2 clauses as input
            and that outputs their "resolvent", e.g., for the
            propositional case:

                Res([phi, alpha-bar], [-phi, beta-bar])
                        = [alpha-bar, beta-bar]

            (where "phi" is a propositional wff in CF, and "alpha-bar"
            and "beta-bar" are disjunctions of wffs in CF)

            This is a function that you should be able to implement
            now!

            For the FOL case, we have to have something slightly
            more complex, since we might need to unify the phi's
            before resolving them.  Let's suppose that UNIF is our
            unification algorithm (which we have not yet covered
            in lecture).  Then the resolution function for FOL looks
            like this:

                Res([UNIF(phi1), alpha-bar], [-UNIV(phi2), beta-bar])
                        = [alpha-bar, beta-bar]

            (where "phi1" and "phi2" are wffs in CF that need to be
            unified before being able to resolve them; when they are
            unified, UNIF(phi1) will be identical to UNIF(phi2), so
            in the 2 input clauses to Res, we'll have a wff and its
            negation, just as we do in the propositional case).

            Note, therefore, that this version of Res includes the
            propositional case, since, in the propositional case,
            phi1=phi2 to begin with and since UNIF(phi), where phi
            is a propositional wff is just phi itself (there are no
            variables to substitute for).

            This means that you can, right now, write your version
            of Res, using a "stub" procedure for UNIF.  In the
            propositional case, it will just return its argument
            (i.e., it will be a no-op), and in the FOL case, for
            now, it can return an error message ("Sorry, this is
            not yet implemented").  Then, when you feel comfortable
            about writing UNIF, you can just plug it in.

2.  There is also the issue of combining all of these into a single
program that takes as input an argument S |- alpha and uses refutation,
resolution, and unification (applied to the CF forms of S and -alpha)
to determine, by deriving [], whether alpha follows from S.  You can
leave that for last.  The CF algorithm can stand on its own.  The Res
algorithm can either take its input pairs from the user, or can offer
the user a choice of wffs from CF(S) union CF(-alpha) (unioned with
any new wffs derived via resolution of previous wffs), ending when [] is
added to the set.

3.  There are also the individual exercises that, in the project specs,
I have asked you to do at least by hand whether or not you are able to
complete the implementation.  Most of those can be done now (the unification
examples can wait till we cover it in class).

4.  Finally, there's the report.  Don't wait till the last minute on
this!  There's no reason you couldn't start writing the report now,
describing what each module does and how they fit together, inserting
the actual code and sample runs as they become available.  Even if you
fail to complete any of the implementations, you can still have a
report!  (Of course, in that case, it should have a section describing
the bugs in whatever code you do have, and how you would have tried
eliminating those bugs had I given you yet another extension :-)