CIS 554 Clojure 2: Resolution
Fall 2015, David Matuszek
Purposes of this assignment
- To give you more practice in Clojure
- To consolidate your understanding of resolution
Write a Clojure program to do resolution. Use the program to solve
sorites (plural, soriteses)
is a kind of logic puzzle. Lewis Carroll (the mathematician and author of
Alice in Wonderland) wrote a book called Symbolic Logic and
the Game of Logic in which he presented a large number of
soriteses. Here is an example:
- All my sons are slim.
- No child of mine is healthy who takes no
- All gluttons, who are children of mine, are
- No daughter of mine takes any exercise.
can be turned into a set of clauses in predicate calculus by
- using consistent terminology (fat = not slim,
daughter = not son),
- changing each sentence into an implication,
- changing implications into clauses by using
the identity (A ⇒ B = ¬ A ∨ B).
(Note: ⇒ means implies,
¬means not, and ∨
means or.) So,
| 1. All my sons are slim.
|| son ⇒ slim
|| ¬son ∨ slim
| 2. No child of mine is healthy who takes no
|| ¬exercise ⇒ ¬healthy
|| exercise ∨ ¬healthy
| 3. All gluttons, who are children of mine, are fat.
|| glutton ⇒ ¬slim
|| ¬glutton ∨ ¬slim
| 4. No daughter of mine takes any exercise.
|| ¬son ⇒ ¬exercise
|| son ∨ ¬exercise
is another sorites:
- Animals, that do not kick, are always
- Donkeys have no horns.
- A buffalo can always toss one over a
- No animals that kick are easy to
- No hornless animal can toss one over
- All animals are excitable, except
Constants can be represented in various ways: as atoms (
"exercise"), or keywords (
in some other fashion, as long as they can be tested for equality.
For general resolution, you have to represent variables.
For this purpose, we will use small integers (
3, ...). Integers are easy to test for, and do not occur in
logic problems. As always, when resolving clauses, you must remember to
standardize variables apart--the scope of a variable is the clause in which
it occurs, so a
1 in one clause is a different variable from
1 in another clause.
A predicate is a list of two or more things, where the
first thing is a constant other than
not. For example,
mary bob) or
(sameweight 1 2). Variables
may occur as the "arguments" to predicates (after the first thing in the
list), and nowhere else.
A literal is a constant, variable,
or predicate, or the negation of a constant, variable,
or predicate. Represent negations with
A clause is the disjunction ("or") of zero or more
literals. Represent a clause as a list of literals, for example,
(not :healthy)). There is no need to represent the "or" explicitly.
To have a consistent representation, a clause consisting of a single literal
is still in a list; a clause containing no literals is the empty list,
Finally the--let's call it a database--is a list of
clauses. A sorites is an initial database, before
resolutions have added more clauses to it.
- Returns the resolution of the two clauses. The clauses may contain
variables. (Note: This function is not required to solve a sorites, as a
sorites does not contain variables.) To resolve clauses containing
variables, you will need to implement Prolog-style unification.
- Returns the resolution of the two clauses. The clauses will not
- Returns a clause which is the "solution" of the sorites.
What is a "solution"? I believe that if you continue performing
resolutions until you have used every clause in the initial database
(possibly some of them more than once) in the construction of a clause,
that clause will be unique, and can be considered to be the solution.
Note: You will need a helper function or
functions with additional parameters.
Unit testing is recommended, but optional.
Zip and turn in your
resolution-test.clj files by 6am, Wednesday September
30. If you do not do unit testing, or if you put your unit
tests in the same file, just turn in your unzipped
As always, only files submitted to Canvas
will be accepted. I do not accept assignments submitted by email.