User Tools

Site Tools


teaching:is:ind-solutions

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
teaching:is:ind-solutions [2020/06/24 16:16]
Franconi Enrico [12.6]
teaching:is:ind-solutions [2020/06/24 17:11] (current)
Franconi Enrico [12.9]
Line 89: Line 89:
 (b) (b)
      
-  yes(R) ⇐ next_door(R,r107) +  yes(R) ⇐ next_door(R,r107)  (*
-     resolve with two_doors_east(E1,W1) ← +     resolve with next_door(E1,W1) ⇐ imm_east(E1,W1). 
-          imm_east(E1,M1) ∧imm_east(M1,W1). +     substitution: {E1/R,W1/r107
-     substitution: {E1/r107,W1/R+  yes(R) ⇐ imm_east(R,107)
-  yes(R) ⇐ imm_east(r017,M1∧imm_east(M1,R) +
-     select leftmost conjunct+
      resolve with imm_east(E2,W2)←imm_west(W2,E2)      resolve with imm_east(E2,W2)←imm_west(W2,E2)
-     substitution: {E2/r107,W2/M1+     substitution: {E2/r105,W2/R
-  yes(R) ⇐ imm_west(M1,r107) ∧imm_east(M1,R) +  yes(R) ⇐ imm_west(r107,R) 
-     select leftmost conjunct+     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)      resolve with imm_west(r105,r107)
-     substitution: {M1/r105} +     substitution: {R/r105} 
-  yes(R) ⇐ imm_east(r105,R) +  yes(r105) ⇐  
-     resolve with imm_east(E3,W3)imm_west(W3,E3+ 
-     substitution: {E3/r105,W3/R} + 
-  yes(R) ⇐ imm_west(R,r105+<nowiki>(c)</nowiki> 
-     resolve with imm_west(r103,r105+ 
-     substitution: {R/r103+...similar to (d)... 
-  yes(r103) ⇐ + 
 +(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 ===== ===== 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 ===== ===== 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 ===== ===== 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) <-
teaching/is/ind-solutions.1593008174.txt.gz · Last modified: 2020/06/24 16:16 by Franconi Enrico