CS322 Fall 1999
Module 3 (Reasoning with Symbols)
Assignment 3

Due: 1:30pm, Monday 27 September 1999.

The aim of this assignment is to learn about proof procedures, and how to compute logical consequences.

We will discuss this assignment in Monday's class. Please be prepared to play your part in the discussion. You are to hand in this assignment at the end of the lecture.

Question 1

The file plumbing2.pl (also available in ~cs322/cilog/) contains a CILog axiomatization for the solution to assignment 1, with denotations and tap positions given below:
The Plumbing Domain
  1. Give a sequence of atoms added to the consequence set for a bottom-up proof procedure. Show clearly what is the consequence set.
  2. Give a top-down derivation for the query
  3. Give a failing derivation for the query ?flow(d1).

Question 2

Consider the following Datalog program (also available here):
attends(P,D) <- proctors_exam(P,C) & exam(C,D).
proctors_exam(P,C) <- instructor(P,C).
proctors_exam(P,C) <- teaching_assistant(P,C).
CILog always selects the leftmost conjunct to resolve, and always chooses the topmost clause that leads to a solution.
  1. Give a top-down derivation, showing all substitutions, for the first answer for the query:
    Specify which clause was chosen at each stage.
  2. Give a top-down derivation, showing all substitutions, for the second answer for the same query. Only show the part of the derivations that is not shared with the first answer.

Question 3

For each question in this assignment, say how long you spent on it. Was this reasonable? What did you learn?
David Poole