Course Description

This course is an introduction to logic programming and automated theorem proving, with connections made to AI. Rather than hazard a precise definition of LP and ATP, let me define it ostensively here, that is, let me define it through an example of something that would fall under this topic:

A zoo curator is selecting animals to import for the zoo's annual summer exhibit. Exactly one male and one female of each of the following types of animal are available: hippo. llama, monkey, ostrich, panther. The following restrictions apply:

• If no panthers are selected, then both ostriches must be selected.
• A male panther cannot be selected unless a female llama is selected.
• If a male monkey is selected, then neither a female ostrich nor a female panther may be selected.
• At least one hippo must be selected.

Which one of the following is an acceptable selection of animals for the exhibit?

female hippo, female monkey, male monkey, male ostrich, male panther

female hippo, male llama, female monkey, female ostrich, male ostrich

male hippo, female llama, male llama, female monkey, female ostrich

male hippo, female llama, male monkey, female panther, male panther

female llama, male llama, male monkey, female ostrich, male panther

A logic-based system able to solve this problem, and prove that the solution is correct, would fall under the title of this course. Success would be especially impressive for a system able to go from the English to the solution and proof, without help from a human who carries out the translation from the English to the logic. As a brief preview, here is how the third restriction might be represented in OTTER, a theorem prover that is able to solve this problem (and one that will play a large role in this course):

all x (((Selected(x) & Male(x) & Monkey(x)) ->

((- (exists y (Selected(y) & Female(y) & Ostrich(y)))) &

(- (exists y (Selected(y) & Female(y) & Panther(y))))))

Of course, the domains will vary. Logic programming and automated reasoning can be applied to puzzles like this, as well as to the control of a robot, the design of circuits, and longstanding problems in higher mathematics.

There are a number of ways to pursue implementation in logic programming and automated theorem proving, including,

1. Use Prolog and its variations and refinements.
2. Use another high-level language like Lisp.
3. Use theorem provers (and, when necessary, connect them to code written in an appropriate high-level language, e.g., Lisp).

While I will make some comments about 1 and 2 (and while to some degree we may even take route 2), we will pursue route number 3 in this course.