CIS 554 Tips for Clause Form Assignment
Fall 2012, David Matuszek

I've been working on the Clause Form Assignment, and it's challenging. I thought I would share with you some helper methods that I wrote. You are welcome to include these in your code. Use at your own risk.

A Pattern Matching function

One of the rules (there are others) for reducing the scope of negations (step 2) is: ¬(¬p) ≡ p. In Clojure terms, this means that (not (not p)) should be rewritten as p. Here is my first version of a function to do this:

(defn reduce-scope-of-negation [expr]
    (if (and (list? expr) (not (empty? expr)))
        (if (and (= (first expr) 'not) (= (first (second expr)) 'not))
            (second (second expr))
            expr )
        expr ) )

(ns user (:use clojure.test))

(deftest test-reduce-scope-of-negation
    (is (= 'p (reduce-scope-of-negation 'p)))
    (is (= 'p (reduce-scope-of-negation '(not (not p)))))

This works, but it's ugly! And that's only one simple case. I hate to think about writing an entire program like this. What, oh what, is to be done?

It would be easy enough in Prolog:

reduce(not(not(P)), P).

Fortunately, Clojure is a kind of Lisp, so we can do something about this! Let's write a simple pattern-matching function.

(defn matches [expr pattern]
    (and (list? expr) (list? pattern))
        (empty? expr) (empty? pattern)
        (empty? pattern) false
        :else (and (matches (first expr) (first pattern))
                   (matches (rest expr) (rest pattern))) )
   (= pattern '_) true
   :else (= expr pattern) ) )

The unit test should explain well enough what this function does:

(defn is-not [x] (is (not x)))

(deftest test-matches
  (is (matches 'a '_))
  (is-not (matches '_ 'a))
  (is (matches 'p 'p))
  (is (matches '(a b c) '_))
  (is (matches '(a (b c) d) '(_ (b _) d)))
  (is (matches '(a (b c) d) '(_ _ d)))
  (is-not (matches '(a (b c) d) '(a (b _ c) d)))

And here's an example of its use:

(defn reduce-scope-of-negation [expr]
  (if (matches expr '(not (not _)))
    (second (second expr))
    expr ) )

Boy, that looks better!

The matches function is useful in many places throughout this assignment; feel free to copy it and use it.

Simplifying the conversion functions

The reduce-scope-of-negation works when applied directly to a double negation, such as (not (not p)). It obviously isn't going to work for more complicated expressions, where there may be many deeply nested double negations. Here's what I think we need to do in that case:

  1. Try to apply the rule to the entire expression, generating a (possibly) new expression.
  2. Recursively apply the rule to all subparts of the new expression.

Well, we can write a function that recursively applies reduce-scope-of-negation. But that's only one of nine rules that have to be applied. Do we have to do that for all of them?

Again, Clojure comes to the rescue. It's a functional language. And reduce-scope-of-negation is just a function. What we can do for one function, we can do for any function! So let's do it...

(defn apply-at-all-levels [f expr] ; f must be applicable to lists
  (let [apply-if-list (fn [e] (if (list? e) (f e) e))
        top (apply-if-list expr)]
      (= top ())   ()
      (list? top)  (cons (apply-at-all-levels f (first top))
                         (apply-at-all-levels f (rest top)) )
      true         top ) ) )
(deftest test-apply-at-all-levels
  (let [app apply-at-all-levels]
    (is (= 'p (app reduce-scope-of-negation ' p)))
    (is (= 'p (app reduce-scope-of-negation '(not (not p)))))
    (is (= '(f p) (app reduce-scope-of-negation '(f (not (not p))))))
    (is (= '(not (a (fun b)))
           (app reduce-scope-of-negation
           	   '(not (a (not (not (fun (not (not b)))))))) )) ) )

Here's a bit of explanation:

  1. The two arguments to apply-at-all-levels are a function, f, and an expression, expr.
  2. The let defines local variables. The form is (let [variable value ... variable value] expression) The values are computed sequentially (in order), then are used as local variables in the expression.
  3. (fn [e] (if (list? e) (f e) e)) is a function literal.
    1. This is a function that, when called with some list e, will return the result of applying f to e. When called with something that isn't a list, it will return its argument unchanged.
    2. The newly-created function is assigned to the local variable apply-if-list.
  4. The next line calls the function apply-if-list with the argument expr, and defines top to have the resultant value.
  5. If the result top is:

This is another function that I think will be very handy in this assignment. As Clojure functions go, it is fairly complicated, and the unit tests aren't very complete, so use at your own risk! If you find errors or improvements, please post them on Piazza--after careful testing, of course!

More tips


user=> (add-all '(1 2 3 4 5))
java.lang.IllegalStateException: Var user/add-all is unbound. (NO_SOURCE_FILE:0)

Clojure has a problem that I haven't seen in any other modern language. As in C, the definition of a function must occur earlier in the file than any call to the function. In this case, my add-all calls a helper function, help-add-all, which occurs after add-all in the file.

This is particularly confusing if you have been trying things in a REPL, because you may be using an earlier version of your called function. Then when you try to run the program later, it fails because your functions are in the wrong order.

To fix this, use the declare special form. For example, if I put (declare help-add-all) before I define add-all, then Clojure knows that help-add-all will be defined, and my add-all function compiles correctly.

Unit testing

I strongly recommend that you do exhaustive unit testing on your functions! I don't believe that you can finish this assignment if you don't. This is a big program built up out of a lot of little pieces, and all the little pieces have to work perfectly in order for the program to work.

See the first block of code (reduce-scope-of-negation) above for the form of unit tests. Don't forget the (ns user (:use clojure.test)) before everything, or the (run-tests) afterward.

We will test your program using my unit tests. I specified only the single top-level function, clausify. Consequently I won't know the names of any of your smaller functions, and won't be able to test them. I can only test clausify. My tests are likely to look something like

(deftest test-clausify-eliminate-double-negation
  (is (= '(p) (clausify 'p))) 
  (is (= '(p) (clausify '(not (not p)))))

Remember, clausify is supposed to return a list of clauses, so the result in both cases should be (p), not p.

(deftest test-clausify-example
  (is (= '(forall x
    (implies (and (roman x) (know x marcus))
             (or (hate x caesar)
                 (forall y (exists z
                           (implies (hate y z))
                                    (think-crazy x y) ))) ) )
    '( (not (roman x))  (not (know x marcus))  (hate caesar)
       (not (hate y z)) (think-crazy x y) ) )) )

The above is just to show you what my unit tests will look like; I don't know for sure that this is the correct result. Also, your clauses may be in a different order than mine, so my unit tests will have to permit that.


Remember, good programmers are "creatively lazy." I wrote matches and apply-at-all-levels to save myself work. Since doing the above, I've done other things to simplify my code.

My advice: When you are writing something that's big and ugly, stop for a moment, and think about what you wish you had to make it easier. Then go write that thing. The overall savings in time and effort can be tremendous.


I don't know of a good way to interactively step through code to see where it is going wrong. And just staring at the code doesn't help all that much.

There is, however, a way to trace the code.

(use 'clojure.contrib.trace)

(dotrace [reduce-scope-of-negation]
   (reduce-scope-of-negation '(not (and a b))) )

The arguments to dotrace are the functions you want to trace, and the body is a call to one of those functions.

Here is something that is much better than dotrace: For each function that you wish to trace, replace defn with dotrace:

(deftrace [reduce-scope-of-negation]
   (reduce-scope-of-negation '(not (and a b))) )


Use a decent text editor!