====== Solutions to the Individuals and Relations lab ======

===== 12.3 =====
<code>
C={r(a),r(e),p(c),q(b),s(a,b),s(d,b),s(e,d)}

C ∪ {q(a)} by rule 2 with X/a,Y/b

C ∪ {p(a)} by rule 1 with X/a

C ∪ {q(d)} by rule 2 with X/d,Y/b

C ∪ {q(e)} by rule 2 with X/e,Y/d

C ∪ {p(e)} by rule 1 with X/e

</code>
===== 12.4 =====

  yes(R) ⇐ two_doors_east(R,r107)
     resolve with two_doors_east(E1,W1) ←
          imm_east(E1,M1) ∧imm_east(M1,W1).
     substitution: {E1/R,W1/r107}
  yes(R) ⇐ imm_east(R,M1) ∧imm_east(M1,r107)
     select leftmost conjunct
     resolve with imm_east(E2,W2)←imm_west(W2,E2)
     substitution: {E2/R,W2/M1}
  yes(R) ⇐ imm_west(M1,R) ∧imm_east(M1,r107) (*)
     select leftmost conjunct
     resolve with imm_west(r107,r109)
     substitution: {M1/r107,R/r109}
  yes(r111) ⇐ imm_east(r107,r107)
     resolve with imm_east(E3,W3)←imm_west(W3,E3)
     substitution: {E3/r107,W3/r107}
  yes(r111) ⇐ imm_west(r107,r107)
     no substitution available
     BACKTRACK to (*) with another resolvent, 
        until imm_west(r107,r109) is chosen 

===== 12.5 =====

By selecting the rightmost conjunct, there would be only one choice: 

  yes(R) ⇐ two_doors_east(R,r107)
     resolve with two_doors_east(E1,W1) ←
          imm_east(E1,M1) ∧imm_east(M1,W1).
     substitution: {E1/R,W1/r107}
  yes(R) ⇐ imm_east(R,M1) ∧imm_east(M1,r107)
     select rightmost conjunct
     resolve with imm_east(E2,W2)←imm_west(W2,E2)
     substitution: {E2/M1,W2/r107}
  yes(R) ⇐ imm_east(R,M1) ∧imm_west(r107,M1)
     select rightmost conjunct
     resolve with imm_west(r107,r109)
     substitution: {M1/r109}
  yes(R) ⇐ imm_east(R,r109)
     resolve with imm_east(E3,W3)←imm_west(W3,E3)
     substitution: {E3/R,W3/r109}
  yes(R) ⇐ imm_west(r109,R)
     resolve with imm_west(r109,r111)
     substitution: {R/r111}
  yes(r111) ⇐ 
  
It is optimal because the query had a constant in its second argument, therefore instantiating the variable W of the two_doors_east predicate. But it would not be optimal for queries like:

  ask two_doors_east(r107,R).
===== 12.6 =====
(a)
  yes(R) ⇐ two_doors_east(r107,R)
     resolve with two_doors_east(E1,W1) ←
          imm_east(E1,M1) ∧imm_east(M1,W1).
     substitution: {E1/r107,W1/R}
  yes(R) ⇐ imm_east(r017,M1) ∧imm_east(M1,R)
     select leftmost conjunct
     resolve with imm_east(E2,W2)←imm_west(W2,E2)
     substitution: {E2/r107,W2/M1}
  yes(R) ⇐ imm_west(M1,r107) ∧imm_east(M1,R)
     select leftmost conjunct
     resolve with imm_west(r105,r107)
     substitution: {M1/r105}
  yes(R) ⇐ imm_east(r105,R)
     resolve with imm_east(E3,W3)←imm_west(W3,E3)
     substitution: {E3/r105,W3/R}
  yes(R) ⇐ imm_west(R,r105)
     resolve with imm_west(r103,r105)
     substitution: {R/r103}
  yes(r103) ⇐ 
  
(b)
  
  yes(R) ⇐ next_door(R,r107)  (*)
     resolve with next_door(E1,W1) ⇐ imm_east(E1,W1).
     substitution: {E1/R,W1/r107}
  yes(R) ⇐ imm_east(R,107)
     resolve with imm_east(E2,W2)←imm_west(W2,E2)
     substitution: {E2/r105,W2/R}
  yes(R) ⇐ imm_west(r107,R)
     resolve with imm_west(r107,r109)
     substitution: {R/r109}
  yes(r109) ⇐ 
  
Another derivation by backtracking to (*) and selecting another clause to resolve against:

  yes(R) ⇐ next_door(R,r107)
     resolve with next_door(W1,E1) ⇐ imm_west(W1,E1).
     substitution: {W1/R,E1/r107}
  yes(R) ⇐ imm_west(R,r107)
     resolve with imm_west(r105,r107)
     substitution: {R/r105}
  yes(r105) ⇐ 


<nowiki>(c)</nowiki>

...similar to (d)...

(d)

  yes(R) ⇐ west(r107,R)  (*)
     resolve with west(W1,E1) ⇐ imm_west(W1,E1).
     substitution: {W1/r107,E1/R}
  yes(R) ⇐ imm_west(r107,R)
     resolve with imm_west(r107,r109)
     substitution: {R/r109}
  yes(r109) ⇐ 
   
Another derivation by backtracking to (*) and selecting another clause to resolve against:

  yes(R) ⇐ west(r107,R)  (*)
     resolve with west(W1,E1) ⇐
          imm_west(W1,M1) ∧
          west(M1,E1).
     substitution: {W1/r107,E1/R}
  yes(R) ⇐ imm_west(r107,M1) ∧ west(M1,R).
     select leftmost conjunct
     resolve with imm_west(r107,r109)
     substitution: {M/r109}
  yes(R) ⇐ west(r109,R).
    resolve with west(W2,E2) ⇐ imm_west(W2,E2).
     substitution: {W2/r109,E2/R}
  yes(R) ⇐ imm_west(r109,R)
     resolve with imm_west(r109,r111)
     substitution: {R/r111}
  yes(r111) ⇐ 

===== 12.8 =====

(a) 
  f(X,X,c,X,c)


(b) 
  yes(c(l,X1),L) ⇐ append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil)))))


<nowiki>(c)</nowiki> 

  append(c(l,X1),c(L,nil),c(l,c(i,c(s,c(t,nil))))) ⇐ 
     append(X1,c(L,nil), c(l,c(i,c(s,c(t,nil)))))

===== 12.9 =====

(a)
  {Z/f(X),Y/g(b)}

(b)
  {W/f(t),X/t,Q/t}

<nowiki>(c)</nowiki>

  {P/val(X,bb),Z/val(X,bb)}

===== 12.14 =====

(a) Here is a top-down derivation:

  yes(Y) ⇐ adj(b,Y,c(a,c(b,c(b,c(a,emp))))).
    choose clause 3, with { A/b,B/Y,L/c(a,c(b,c(b,c(a,emp)))),F/F1,E/E1 }
    
  yes(Y) ⇐ ap(F1,c(b,c(Y,E1)),c(a,c(b,c(b,c(a,emp)))))
    choose clause 2, under
    { F1/c(a,T2),L/c(b,c(Y,E1)),H/a,R/c(b,c(b,c(a,emp))),T/T2 } 
    
  yes(Y) ⇐ ap(T2,c(b,c(Y,E1)),c(b,c(b,c(a,emp))))   (*)
    choose clause 1 under { T2/emp,Y/b,E1/c(b,c(a,emp)) } 
    
  yes(b) ⇐

(b) Yes, there is one more answer .

  at (*) 
    choose clause 2 under 
    { T2/c(b,T3),L/c(b,c(Y,E1)),H/b,R/c(b,c(a,emp)),T/T3 } 
    
  yes(Y) <- ap(T3,c(b,c(Y,E1)),c(b,c(a,emp))) 
    choose clause 1 under { T3/emp,L/c(b,c(a,emp)),Y/a,E1/emp 
    
  yes(a) <-