A demonstration of automatic decomposition of universally quantified constraints according to the "disjunctive embedding" pattern. Constraints are specified as facts in the forall(Bindings,Expression) predicate. In this example, I encode the reflexivity, symmetry, and transitivity aspects of the definition of an equality relation in a simple gra…

lazy_graph.lp

#begin_lua
  function args(t)
    if Val.type(t) == Val.FUNC then
      local res = t:args()
      res.n = nil
      return res
    else
      return {}
    end
  end
  function name(t)
    if Val.type(t) == Val.FUNC then
      return Val.new(Val.ID,t:name())
    else
      return {}
    end
  end

  function contains(term,item)
    for k,v in pairs(term:args()) do
      if tostring(v)==tostring(item) then
        return 1
      end
    end
    return 0
  end
#end_lua.

node(1..5).
potential_label(eq).
{ label(A,Label,B):potential_label(Label) } :- node(A;B).

forall(nodes(a), (a,eq,a)). % reflexivity
forall(nodes(a,b), equivalent((a,eq,b),(b,eq,a))). % symmetry
forall(nodes(a,b,c), implies(and((a,eq,b),(b,eq,c)),(a,eq,c))). % transitivity

connective(equivalent;implies;and;or;nawt).

expr(N,E) :- forall(N,E).
sub_expr(N,E,@args(E)) :- expr(N,E), connective(@name(E)).
expr(N,SubE) :- sub_expr(N,E,SubE).

resolve(N,@args(both(A,B))) :- expr(N,(A,_,B)).
resolve(N,@args(both(A,B))) :- expr(N,eq(A,B)).

var(K) :- resolve(N,K), @contains(N,K)==1.
bind(K,V):node(V) :- var(K).
bind(K,V) :- bot, var(K), node(V).
bound(N,K,V) :- resolve(N,K), @contains(N,K)==1, bind(K,V).
bound(N,K,K) :- resolve(N,K), @contains(N,K)==0.

sat(N, (A,Label,B)) :- expr(N,(A,Label,B)), bound(N,A,AVal), bound(N,B,BVal), label(AVal,Label,BVal).
sat(N,E) :- expr(N,E), @name(E)==and, sat(N,SubE):sub_expr(N,E,SubE).
sat(N,E) :- expr(N,E), @name(E)==or, sat(N,SubE), sub_expr(N,E,SubE).
sat(N,implies(P,Q)) :- expr(N,implies(P,Q)), unsat(N,P).
sat(N,implies(P,Q)) :- expr(N,implies(P,Q)), sat(N,Q).
sat(N,equivalent(P,Q)) :- expr(N,equivalent(P,Q)), sat(N,P), sat(N,Q).
sat(N,equivalent(P,Q)) :- expr(N,equivalent(P,Q)), unsat(N,P), unsat(N,Q).
sat(N,nawt(P)) :- expr(N,nawt(P)), unsat(N,P).

unsat(N, (A,Label,B)) :- expr(N,(A,Label,B)), bound(N,A,AVal), bound(N,B,BVal), not label(AVal,Label,BVal).
unsat(N,E) :- expr(N,E), @name(E)==and, unsat(N,SubE), sub_expr(N,E,SubE).
unsat(N,E) :- expr(N,E), @name(E)==or, unsat(N,SubE):sub_expr(N,E,SubE).
unsat(N,implies(P,Q)) :- expr(N,implies(P,Q)), sat(N,P), unsat(N,Q).
unsat(N,equivalent(P,Q)) :- expr(N,equivalent(P,Q)), sat(N,P), unsat(N,Q).
unsat(N,equivalent(P,Q)) :- expr(N,equivalent(P,Q)), unsat(N,P), sat(N,Q).
unsat(N,nawt(P)) :- expr(N,nawt(P)), sat(N,P).

counterexample_case(N,E):forall(N,E).
counterexample_case(N,E) :- bot, forall(N,E).

% We want to enforce a for-all property. Any valid counterexample should
% demonstrate bindings that witness a failure of this property. Thus, if the
% current bindings witness the property being satisfied, it ain't a valid
% counterexample!
bot :- counterexample_case(N,E), sat(N,E).

:- not bot.

#hide.
#show label/3.