A demonstration of manually applying the "disjunctive embedding" pattern to a transitive closure problem. The pattern replaces a normal rule with a cubic number of groundings with more complex rules requiring only quadratic groundings. In general, the pattern changes the worst-case number of groundings from O(n^|unique_vars_in_rule|) to O(n^max_…

uq_demo.lp

node(1..100).
1 { arc(A,B):node(A):node(B) }.
%arc(A,C) :- arc(A,B), arc(B,C).

%% intent: forall( nodes(a,b,c), implies( and(arc(a,b), arc(b,c)), arc(a,c) ) ). 
var(a;b;c).

bind(V,N):node(N) :- var(V).

bot :- bind(a,A), bind(b,B), not arc(A,B).
bot :- bind(b,B), bind(c,C), not arc(B,C).
bot :- bind(a,A), bind(c,C), arc(A,C).

bind(V,N) :- bot, var(V), node(N).

:- not bot.

#hide.
#show bot.
#show arc/2.
#show bind/2.