- 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).