- Research
- Teaching
- Organisation
This is an old revision of the document!
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
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
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).
(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) ⇐
(c)
…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) ⇐
(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) <-