Differences

This shows you the differences between two versions of the page.

--- teaching:is:ind-solutions [2020/06/24 15:08]
Franconi Enrico [12.5]
+++ teaching:is:ind-solutions [2020/06/24 17:11] (current)
Franconi Enrico [12.9]
@@ Line 66: / Line 66: @@
   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) <-

FranconiSpace

User Tools

Site Tools

Differences

Page Tools