CIS 554 Clojure 2: Resolution
Fall 2015, David Matuszek

Purposes of this assignment

General idea

Write a Clojure program to do resolution. Use the program to solve soriteses.

A 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:

  1. All my sons are slim.
  2. No child of mine is healthy who takes no exercise.
  3. All gluttons, who are children of mine, are fat.
  4. No daughter of mine takes any exercise.

This can be turned into a set of clauses in predicate calculus by

  1. using consistent terminology (fat = not slim, daughter = not son),
  2. changing each sentence into an implication, and
  3. changing implications into clauses by using the identity (A ⇒ B = ¬ A ∨ B).

(Note: ⇒ means implies, ¬means not, and ∨ means or.) So,

Statement Implication Clause
1. All my sons are slim. son ⇒ slim ¬son ∨ slim
2. No child of mine is healthy who takes no exercise. ¬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

Here is another sorites:

  1. Animals, that do not kick, are always unexcitable.
  2. Donkeys have no horns.
  3. A buffalo can always toss one over a gate.
  4. No animals that kick are easy to swallow.
  5. No hornless animal can toss one over a gate.
  6. All animals are excitable, except buffalo.

Details

Constants can be represented in various ways: as atoms (exercise), strings, ("exercise"), or keywords (:exercise), or 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 (1, 2, 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 the 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, (mother 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 (not literal).

A clause is the disjunction ("or") of zero or more literals. Represent a clause as a list of literals, for example, (:exercise (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.

Required functions

(resolve clause1 clause2)
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.
(simple-resolve clause1 clause2)
Returns the resolution of the two clauses. The clauses will not contain variables.
(solve sorites)
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

Unit testing is recommended, but optional.

Due date:

Zip and turn in your resolution.clj and 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 resolution.clj. As always, only files submitted to Canvas will be accepted. I do not accept assignments submitted by email.