Dear All,
I offer a test case to compete with subsumes_term/2 based realization of Picat style rules. I am not against subsumes_term/2 based ideas, but to be convinced, would of course like to see some hard facts, means benchmarking results.
The alternative I see for subsumes_term/2 based ideas is my var/1 indexing. Here is a real world example from a theorem prover:
norm(A, R) :- var(A), !, R = pos(A).
norm((A;B), R) :- !, norm(A, C), norm(B, D), R = or(C,D).
norm((A,B), R) :- !, norm(A, C), norm(B, D), R = and(C,D).
norm((A-:B), R) :- !, norm((-A;B), R).
norm(all(A,B), R) :- !, norm(B, C), R = all(A,C).
norm(exist(A,B), R) :- !, norm(B, C), R = exist(A,C).
norm(-A, R) :- var(A), !, R = neg(A).
norm(- (A;B), R) :- !, norm(-A, C), norm(-B, D), R = and(C,D).
norm(- (A,B), R) :- !, norm(-A, C), norm(-B, D), R = or(C,D).
norm(- (A-:B), R) :- !, norm((A,-B), R).
norm(- all(A,B), R) :- !, norm(-B, C), R = exist(A,C).
norm(- exist(A,B), R) :- !, norm(-B, C), R = all(A,C).
norm(- -A, R) :- !, norm(A, R).
norm(-A, R) :- !, R = neg(A).
norm(A, pos(A)).
One can rewrite it Picat style, and one will possibly find that it needs a few var/1 rules less. But will it also perform? I am happy to see some results. The interesting thing is that var/1 indexing can decide a whole set of subsumes_term/2 tests at once, so this is really a challenge.
Best Regards
Open source:
Maslov Calculus over Herbrandisized Formulas
Prolog flag occurs_check
https://gist.github.com/jburse/ed6eb3316ba1d19309e3711c89dcce3f#file-fitting2-pl