🚀 go-pugleaf

Note that Richard didn't suggest a ground representation, but a
combined representation using ground terms to sort on, but still
including the original terms and their unbound variables.

Using Richard's proposal, equivalence can be tested for (in
Quintus Prolog) using the predicate subsumes_chk/2 twice, or
by grounding the complete set (including the original terms)
before trying to unify (this is OK, because the sets are
sorted).

> 	[p('$VAR'(0),a)-p(X,a), p('$VAR'(0),b)-p(Y,b)]
> 	[p('$VAR'(0),a)-p(V,a), p('$VAR'(0),b)-p(U,b)]

Would be grounded to:
	[p('$VAR'(0),a)-p('$var'(0),a), p('$VAR'(0),b)-p('$var'(1),b)]
	[p('$VAR'(0),a)-p('$var'(0),a), p('$VAR'(0),b)-p('$var'(1),b)]

They would hence unify. The second example:
>		{p(X, a), p(Y, b)} and
>		{p(X, a), p(X, b)}

represented as:
	[p('$VAR'(0),a)-p(X,a), p('$VAR'(0),b)-p(Y,b)]
	[p('$VAR'(0),a)-p(X,a), p('$VAR'(0),b)-p(X,b)]

would be grounded to:
	[p('$VAR'(0),a)-p('$var'(0),a), p('$VAR'(0),b)-p('$var'(1),b)]
	[p('$VAR'(0),a)-p('$var'(0),a), p('$VAR'(0),b)-p('$var'(0),b)]

They would NOT unify, which is correct, and what you're asking for.

/Jonas Almgren