Go backward to Question 3
Go up to Top

Question 4

[Optional] Modify eval (add a new clause) to allow for user-defined functions.

For example, consider the clauses:

sumsq(X,Y)=X*X+Y*Y <= true.
fact(N)=N*fact(N1) <= N>0 & N1 is N-1.
fact(0)=1 <= true.

then query

ask arprove(X is sumsq(3,4)-fact(4),[],E2).

should return X=1, E2=[].