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

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.

• (and arg1 arg2) -- Logical "∧." For simplicity, and will always have exactly two arguments.
  • Note: As far as your program is concerned, this is data, and has no connection to Clojure's build-in and function (unless you decide to explicitly evaluate it, for some reason.) Similar remarks apply to or, and probably to other functions.
• (or arg1 arg2) -- Logical "∨." For simplicity, or will always have exactly two arguments.
• (not arg1) -- Logical "¬." For simplicity, not will always have exactly one argument.
• (implies arg1 arg2) -- Logical "arg1 ⇒ arg2." For simplicity, implies will always have exactly two arguments.
• (forall x expression) -- Means "∀x, expression," where the expression probably contains occurrences of the atom x.
• (exists x expression) -- Means "∃x, expression," where the expression probably contains occurrences of the atom x.
• (predicate args) -- For predicates such as Roman(x) and know(x, Marcus)

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

• Atoms, such as todayIsSunny or caesarIsEmperor,
• Predicates, such as (roman x) and (know x marcus).
• Two-element lists representing negated atoms or predicates, such as (not todayIsSunny) or (not (know x marcus)), and
• Lists representing Skolem functions, such as (skolem bignumber) or (skolem mother x).

Skolem examples

Skolem functions result from existential (∃) quantifiers.

• If the existential quantifier applies to a variable that is not inside a universal (∀) quantifier, it is essentially a "Skolem constant." For example:
  • "There exists a number x that is greater than 10000" → ∃x, greater-than-10000(x) → (x).
  • We are just picking some variable to stand in for the value that we know exists, we just don't know or care what that value is.
  • More readably: "There exists a number bignumber that is greater than 10000" → ∃bignumber, greater-than-10000(bignumber) → (skolem bignumber).
• If the existential quantifier applies to a variable that is inside a universal quantifier, then the choice of variable depends on the universally quantified variable.
  • Everybody has a mother → For every person x, there exists some person y, such that y is the mother of x → ∀x ∃y is-mother-of(y, x) = (∀x (∃y is-mother-of(y, x))) → (y x).
  • More readably, For every person x, there exists some person mother, such that mother is the mother of x → (skolem mother x).

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.