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 arg1 arg2)-- Logical "
∧." For simplicity,
andwill always have exactly two arguments.
andfunction (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,
orwill always have exactly two arguments.
(not arg1)-- Logical
"¬." For simplicity,
notwill always have exactly one argument.
(implies arg1 arg2)-- Logical "
arg1 ⇒ arg2." For simplicity,
implieswill always have exactly two arguments.
(forall x expression)-- Means "
expression," where the expression probably contains occurrences of the atom
(exists x expression)-- Means "
∃x, expression," where the expression probably contains occurrences of the atom
(predicate args)-- For predicates such as
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
(know x marcus).
(not (know x marcus))
(skolem mother x)
Skolem functions result from existential (∃) quantifiers.
bignumberthat is greater than 10000
x, there exists some person
mother, such that
motheris the mother of
(skolem mother x).
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.