Fall 2012, David Matuszek

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.

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.

Write a function `clausify`

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

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`

-- Logical "*arg1 arg2*)`∧`

." 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`

-- Logical*arg1 arg2*)`"∨`

." For simplicity,`or`

will always have exactly two arguments.`(not`

-- Logical*arg1*)`"¬`

." For simplicity,`not`

will always have exactly one argument.`(implies`

-- Logical "*arg1 arg2*)

." For simplicity,*arg1*⇒*arg2*`implies`

will always have exactly two arguments.`(forall`

-- Means "*x expression*)`∀x,`

," where the expression probably contains occurrences of the atom`expression`

`x`

.`(exists`

-- Means "*x expression*)`∃x,`

," where the expression probably contains occurrences of the atom*expression*`x`

.`(`

-- For predicates such as*predicate**args*)`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.

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

or(not todayIsSunny)

, and(not (know x marcus)) - Lists representing Skolem functions, such as
`(skolem bignumber)`

or(skolem mother x)

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)`

.

- "There exists a number x that is greater than 10000" → ∃x, greater-than-10000(x) →
- 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)`

.

- Everybody has a mother →

Corrected, but may still have errors!

∀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) ))) ) )

¬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) )

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. **