CIS 554 Clojure Assignment 2: Conversion to Clause Form
Fall 2012, David Matuszek

Purposes of this assignment

The purpose of the first Clojure assignment was to get you familiar with the basic Clojure functions, and the typical ways in which those functions are used.

This assignment is intended to give you experience in designing and writing an actual Clojure program. It is a "typical" Lisp assignment, and does not require any special features of Clojure.

General idea of the assignment

Convert a statement in the predicate calculus into clause form.

A brief description of the algorithm is given in the last part of my Prolog 4: Logic slides.

Detailed specification under construction

Write a function clausify that takes one argument, an expression in the predicate calculus, and returns the equivalent list of clauses.

Representation of predicate calculus expressions

An expression in the predicate calculus will be a list, written as a single function call. Any of the following may be the top level call, and may contain nested calls, to any level.

Atoms, such as x, occur as arguments and in expressions. Atoms never occur as the first element of a list.

Representation of clause form

The result returned by clausify will be a list of clauses, where each clause will be a list. This will the the correct form even if there is only one clause.

The elements in the clause will be

Skolem examples

Skolem functions result from existential (∃) quantifiers.

Example from prolog-04-resolution.ppt lecture

Corrected, but may still have errors!

Input to clausify:

∀x, ( [Roman(x) ∧ know(x, Marcus)] ⇒
       [hate(x, Caesar) ∨ (∀y∃z, hate(y, z) ⇒ thinkCrazy(x, y))] )
    '(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) ))) ) )

Output from clausify:

¬Roman(x) ∨ ¬know(x, Marcus) ∨ hate(Caesar) ∨¬hate(y, z)) ∨ thinkCrazy(x, y)
( (not (roman x))  (not (know x marcus))  (hate caesar)
  (not (hate y (skolem z x y))) (think-crazy x y) )

Due date

Your program is due before 6am Wednesday, October 3. Zip up your program file along with some sample inputs, and submit via Blackboard.

Late penalties: There will be a 10 point penalty (out of 100 points) for programs between one minute and one week late, and a 25 point penalty for programs later than one week. At some unspecified time after one week we will stop accepting assignments.

Do not turn in a file in any other format than .zip, such as .rar. Zip files can be unzipped on any platform; .rar and other compressed files require special software.

If you don't have access to Blackboard, get the matter resolved beforehand. I do not, under any circumstances, accept assignments submitted by email.