Needing help with call_with_depth_limit/3

Help! Predicate
9

It’s good to know person interested in (deprecated ? ) call_with_depth_limit.

I found all of old Prolog codes of mine on “Ordered Linear with Ancestor resolution” prover were broken, which used the call_with_depth_limit. So I got
curious of writing a (toy) simple-minded resolution prover, which is based on:

  • iterated deepening ( hand made on simple limited purpose ).

  • prolog like proof search:

    • topdown
    • left-to-right

  • history of literals relolved upon (tabling ?).

Fortunately, functionality of my old codes was
fully recovered. some example queries follows.

% Valid formula.
% ?- F = (all(y, f(y)==p) == (p==all(x, f(x)))), prove(F).
% ?- F = (((f(1)==p) & (f(2) == p)) == (p== (f(1) & f(2)))), prove(F).
% ?- F = (all(A, p==f(A))==(p==all(B, f(B)))), prove(F).
% ?- F = ((p == all(A, f(A))) == all(B, p== f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F).

% Invalid formula.
% ?- prove(all(y, some(x, f(x, y)) -> some(x, all(y, f(x, y))))). % false
% ?- prove((all(X, some(Y, p(X, Y)))->some(Y, all(X, p(X, Y))))).  % false.
% ?- prove((some(X, p(X))->all(X, p(X)))).		% false.

However new codes lacks anything like paramodulation strategy, for which
I have no idea (sigh). So, to prove properties on functions on natural number, for example, it must be very weak.

BTW, I have tried to upload my pack pac as v1.8.9 with this new codes, but failed. It seems that packages manager has been changed.