Assignment 6 information

Code and other information

resolution.scm --- support code for assignment 6. UPDATED AGAIN 11/7/99
Testing program --- see the comments for instructions, caveats, etc. UPDATED AGAIN 11/8/99 (sentence 4 was misformed)
Please note that for the resolution-prove procedure that the proof that you get printed out may not be correct because the sentence-symbol counter is not set properly upon calling resolution-prove and thus there will be duplicate sentences (i.e. two (sentence 1)s, etc.) Despite this problem, if the goal can be proven (i.e. a contradiction reached) your resolution-prove procedure will still find it and will return #t even though the printed proof probably won't make sense.
A few additional tips appear below.
Addenda & errata updated 11/4/99
Please use the line (load "resolution") in your sourcecode.
Although I have asked you not to do this in the past, we are doing things a little differently for this assignment.

Addenda & eratta

There is an error in the subst examples in the assignment handout. They should appear as below:

(subst '((sentence 1) ((v (likes x y) (hates a b)) given))
        '(((x (sentence 1)) John)) 
        '(hates a b))
;Value: (v (likes john y))

(subst '((sentence 2) ((v (eats john meat) (likes alice x)) given))
       '(((x (sentence 3)) fish))
       '(eats john meat))
;Value: (v (likes alice x))

The error was in the format of sentence 1 and sentence 2.

A clarification on substitutions --- a substitution is a list of "var/val" pairs. Each var/val pair has the format:
```
((<var> <sentence-symbol>) <value>)
```
I have added the following accessor functions for var/val pairs:
- (vv-var varval) --- returns the variable
- (vv-ss varval) --- returns the sentence symbol
- (vv-val varval) --- returns the value

Point breakdown and turn-in checklist

(40 points) subst
(70 points) broken down tentatively as follows:
- (30 points) resolution-prove and resolve-sentence
- (40 points) resolve
(30 points) 10 points each for problems (a), (b), and (c). Turn in:
- veg-goal, veg-sos, veg-kb
- likes-goal, likes-sos, likes-kb
- turn in a printout as described in the problem

Problem 3b

Consider the following problem:

Everyone that likes Bob either likes Doug or likes Alice. Everyone that doesn't like Bob likes Doug. Carol doesn't like Doug. Does Carol like Alice?

Define the variables likes-goal, likes-sos, likes-kb to solve this problem using your program.

Problem 3c

Think of this as a bonus problem --- attempt it only if you have finished the rest of the assignment.

Suppose we are playing a 3 by 3 game of minesweeper and we have the following situation:

CA	CB	CC
1	3	CD
0	1	CE

where I have labeled the "unknown" cells CA through CE. For those of you unfamiliar with the game minesweeper (available on Windows and Linux/Gnome computers), the diagram above means that:

one of the two cells CA and CB has a mine
three of the five cells CA, CB, CC, CD, and CE have mines
one of the two cells CD and CE has a mine

Transform this information into first order logic statements using the predicate Mine(x) and the cell names as objects.

Turn in a printout of your initial sos and/or knowledge base. Can you show Mine(CC)? Either turn in a printout of the proof or explain why your program can't do the proof.

Hints

If you aren't using the trace function in Scheme, you should be by this point. It is an invaluable tool for debugging. There are two versions that I use most often: trace-entry and trace. The former will print a message every time the given procedure is entered and will also tell you the arguments for that call. The latter will also print a message when that function returns, giving you the value returned and the arguments for that function call. The untrace function disables this feature. Loading the procedure in question also resets the tracing feature.

Here's some examples:

(define (fac n)
  (if (= n 0)
      1
      (* n (fac (- n 1)))))
;Value: fac

(trace-entry fac)
;No value

(fac 3)
[Entering #[compound-procedure 10 fac]
    Args: 3]
[Entering #[compound-procedure 10 fac]
    Args: 2]
[Entering #[compound-procedure 10 fac]
    Args: 1]
[Entering #[compound-procedure 10 fac]
    Args: 0]
;Value: 6

(trace fac)
;No value

(fac 2)
[Entering #[compound-procedure 10 fac]
    Args: 2]
[Entering #[compound-procedure 10 fac]
    Args: 1]
[Entering #[compound-procedure 10 fac]
    Args: 0]
[1
      <== #[compound-procedure 10 fac]
    Args: 0]
[1
      <== #[compound-procedure 10 fac]
    Args: 1]
[2
      <== #[compound-procedure 10 fac]
    Args: 2]
;Value: 2

; this untraces the procedure fac
(untrace fac)
;No value

; this untraces all procedures
(untrace)
;No value

Unary "or" sentences
Here's the problem: if you have a sentence consisting of a single predicate, it must be given to the subst function as a unary "or" sentence. I.e. instead of giving it:
```
((sentence 10) ((hates alice bob) (sentence 2) (sentence 3) ()))
```
you should give subst the sentence
```
((sentence 10) ((v (hates alice bob)) (sentence 2) (sentence 3) ()))
```
This is because you are probably going to omit this term and what the subst function should return is simply:
```
(v)
```
This is fine because the 0 terms of this unary "or" will be combined with the 1 or more terms of the other sentence to which we're applying resolution. There must be 1 or more terms in the other sentence because otherwise we would get a contradiction. Assuming that the sos and the knowledge base do not initially contain a contradiction, we will have caught any unit contradiction earlier as all unit terms (when generated) are checked for a contradiction.
There are other ways of dealing with this issue, but I think this (or some variation thereon) is the easiest.
I have provided an additional function that you may find useful to deal with this issue.
```
(ns-make-unary-v s)
```
which takes a numbered sentence. If the sentence is a unit sentence, it will be made into a unary "or" sentence, ready to be passed to the subst function. Otherwise, the original sentence will be returned.
I have provided one other function which you can use to negate a sentence:
```
(negate-sentence s)
```
which will negate a plain sentence. This is useful when you negate the goal and add it to the sos at the very beginning.

Here are a few examples you can use until we release the testing program:

(define ns1 '((sentence 1) ((v (eats bob y) (eats pete y)) given)))
(define ns2 '((sentence 2) ((v (eats x meat)) given)))
(define ns3 '((sentence 3) ((v (hates bob x) (eats y vegetables)) given)))
(define ns4 '((sentence 4) ((v (likes john paula) (eats yolanda veg)) given)))

(define sub1 '(((x (sentence 2)) pete) ((y (sentence 1)) meat)))
(define sub2 '(((x (sentence 3)) joe)))
(define sub3 '(((y (sentence 1)) vegetables) ((y (sentence 3)) george)))

(subst ns1 sub1 '(eats pete y))
;Value 1: (v (eats bob meat))

(subst ns2 sub1 '(eats x meat))
;Value 2: (v)

(subst ns3 sub2 '(hates bob x))
;Value 3: (v (eats y vegetables))

(subst ns4 sub2 '(eats yolanda veg))
;Value 4: (v (likes john paula))

(subst ns1 sub3 '(eats pete y))
;Value 5: (v (eats bob vegetables))

(subst ns3 sub3 '(eats y vegetables))
;Value 6: (v (hates bob x))


(define ns5 '((sentence 5) ((~ (eats pete vegetables)) given)))
(define ns6 '((sentence 6) ((v (~ (hates y ralph)) (likes y paula)) given)))
(define ns7 '((sentence 7) ((v (~ (eats yolanda veg)) (likes paula john)) 
given)))

(resolve ns5 ns1)
;Value 7: (((eats bob vegetables) (sentence 5) (sentence 1) (((y (sentence 1)) vegetables))))

(resolve ns6 ns3)
;Value 8: (((v (likes bob paula) (eats y vegetables)) (sentence 6) (sentence 3) (((x (sentence 3)) ralph) ((y (sentence 6)) bob))))

(resolve ns7 ns4)
;Value 9: (((v (likes paula john) (likes john paula)) (sentence 7) (sentence 4) ()))

whuang@cs.rpi.edu
Last updates: October 29; October 26, 1999