I've concluded that the LISP assignment I gave is simply too hard. There were some points I overlooked that made it much more difficult than expected. That's my fault, and I'm sorry.

The old assignment asked you to (1) convert a logical expression in LISP into Conjunctive Normal Form, and (2) simplify the expression. In this revised assignment, you can get full credit by doing either part. If you do both parts, that will be worth 50 points extra credit. (I'm doing it this way so that any work you have already done will not be wasted.)

One of the difficult parts of the assignment is that you may need to apply the same rule over and over again until the expression stops changing. I am providing a function, recursive-apply, that does most of this work for you. This function doesn't do a perfect job, but it does well enough for this assignment. You use it like this:

(recursive-apply 'function expression)

This function takes two arguments, a quoted function name and an S-expression. It applies the function to each top-level list in the expression, recursively, then applies the function to the list of results.
For example, if you have a function remove-implies that replaces (implies p q) with (or (not p) q), then (recursive-apply 'remove-implies expression) will replace all occurrences of (implies p q) everywhere it occurs in the expression. Note: there are certain unusual cases where this function does not do a complete job, but don't worry about that; it's good enough for the current assignment.

Here are some additional functions that you will probably find helpful:

(contains s-expression list)

Tests whether the S-expression is a top-level element of the list. For example, (contains '(x y) '(w (x y) z)) is true, but (contains '(x y) '((w (x y)) z)) is false. This function is like member, but member only tests if an atom is in a list.

(contains-both-x-and-not-x list)

Tests whether the list contains both x and (not x), where x is some arbitrary S-expression that occurs in the list. Note that x is not supplied as a parameter.

Here are some functions for testing your program. Use only the ones you need, depending on whether you are converting to CNF or simplifying (or both). These functions contain test data.

(easy-cnf)

Tests expressions where only a single CNF conversion rule needs to be applied. To use this function, you should either name your function to-cnf or you should change the name used in the auxiliary functions test-cnf and test-combination.


(hard-cnf)

Tests expressions where more than one CNF conversion rule needs to be applied, or the same rule needs to be applied more than once. To use this function, you should either name your function to-cnf or you should change the name used in the auxiliary functions test-cnf and test-combination.


(easy-simplification)

Tests expressions where only a single simplification rule needs to be applied. To use this function, you should either name your function simplify or you should change the name used in the auxiliary functions test-simplify and test-combination.


(hard-simplification)

Tests expressions where more than one simplfication rule needs to be applied, or the same rule needs to be applied more than once. To use this function, you should either name your function simplify or you should change the name used in the auxiliary functions test-simplify and test-combination.

Finally, I've written one function for you for doing transformation to CNF, remove-implies, and one for doing simplification, simplify-contradiction. I hope you can use these as models in writing the other functions. I've also written the beginnings of the functions to-cnf and simplify. As you extend these functions, remember that the result of one function can be given to another function as argument, for example (f (g (h x))).

Finally, the source code for all this is at http://www.csc.vill.edu/~dmatusze/8310summer2001/assignments/tests.lsp.