Go backward to Question 2
Go up to Top
Go forward to Question 4

Question 3

Define arprove(Body,E1,E2) that is true if the Body can be proved with initial environment E1 and resulting environment E2. The only CILog built-in predicate you can use is >.

For example, suppose the knowledge base is:

addato(X,Y) <= Y is X+a.
foo(X,Y) <= X is a+3 & assign(a,X) & Y is a+3.

The query

ask arprove(addato(3,Y),[val(a,4),val(b,5),val(c,7)],E2).

should return Y=7 and E=[val(a,4),val(b,5),val(c,7)].

The query

ask arprove(foo(X,Y),[val(a,4),val(b,5),val(c,7)],E2).

should return X=7, Y=10, E2=[val(a,7),val(b,5),val(c,7)].

Solution

David Poole