AI: Solution Set 4

Assigned: Mar. 9
Due: Mar. 30

Let L be the following first-order language, over a universe of whole numbers.

l(X,Y) --- Predicate. X is less than or equal to Y.
p(X,Y) --- Function. X+Y.
0, 1, 5, 8 --- Constants.
Consider the following axioms:

Problem 1

Give a backward-chaining proof of l(p(5,1), p(p(1,1),8)).
G0: ~l(p(5,1),p(p(1,1),8)              Resolve with H. X1->p(5,1), Y1->p(p(1,1),8)
G1: ~l(p(5,1),Y1) V ~l(Y1,p(p(1,1),8)) Resolve with F. X2->5, Y2->1, Y1->p(1,5).
G2: ~l(p(1,5),p(p(1,1),8).             Resolve with G. X3->1, Y3->5, W3->p(1,1),Z3->8.
G3: ~l(1,p(1,1)) V ~l(5,8)             Resolve 2nd literal with B
G4: ~l(1,p(1,1)).                      Resolve with H. X4->1,Z4->p(1,1)
G5: ~l(1,Y4) V ~l(Y4,p(1,1)).          Resolve with D. X5->1, Y4->p(1,0).
G6: ~l(p(1,0),p(1,1))                  Resolve with G. X6->1, Y6->0, W6->1,Z6->1
G7: ~l(1,1) V ~l(0,1)                  Resolve with C. X7->1
G8: ~l(0,1).                           Resolve with A.
G9: empty.

Problem 2

Give a forward-chaining proof of l(p(5,1), p(p(1,1),8)).

Note: In each of the following, the variables in the rule are renamed, the variables in the fact remain the same.

Resolve C with G, X1->X, Y1->X, giving           J1: ~l(W1,Z1) V l(p(X,W1),p(X,Z1)).
Resolve A with J1, W1->0, Z1->1 giving           J2: l(p(X,0),p(X,1)).
Resolve D with H, X2->X, Y2->p(X,0) giving       J3: ~l(p(X,0),Z2) V l(X,Z2).
Resolve J2 with J3, Z2->p(X,1), giving           J4: l(X,p(X,1)).
Resolve G with J4, X3->X, Y3->p(X,1), giving     J5: ~l(W3,Z3) V l(p(X,W3),p(p(X,1),Z3).
Resolve B with J5, W3->5, Z3->8, giving          J6: l(p(X,5),p(p(X,1),8)).
Resolve F with H, X4->p(X,Y), Y4->p(Y,Z) giving: J7: ~l(p(Y,X),Z4) V l(p(X,Y),Z4).
Resolve J6 with J7, Y5->X, X5->5, Z4->p(p(X,1),8) giving:
                                                 J8: l(p(5,X),p(p(X,1),8)).
J8 and the negated goal resolve to the empty clause under the binding X->1.