Feature request: Support asserting unique name assumption for KB and support equality/inequality in rule bodies in that case

[alanruttenberg]

Relating, sort of, to #5, I had another thought:

If the KB is able to be told the unique name assumption holds in a particular case I think it could be very little work to support equality/inequality testing in rule body. I'm thinking this because you wouldn't have to add new structures to manage equality in general as equality/inequality is completely determined and easily testable in that case.

It would still be worth signaling an exception if equality is asserted in the head, since there more issues there (I imagine).

At least in my case, this would be quite useful gain in expressivity. I think it is the common case that unique names are assumed, so the increased expressivity could benefit other as well.

I guess I could manage this myself via using pseudo equality/inequality predicates and adding the extra assertions to any kb I have, and I may do that, but thought it was worth a mention.

[alanruttenberg]

More work for inequality - didn't remember that there's no negation in rule bodies, so DLGP language would need to be extended to support !=

Ok, not little work. Feel free to close.

[sipi]

Hi Alan, yes, I think I can do that.

We already have a method to preprocess equality in ConjunctiveQuery (in EqualityUtils.java), so it's quite easy to rewrite rule to erase equality in body. p(X,Z) :- q(X,Y), q(Y,Z), X=Z. becomes p(X,X) :- q(X,Y), q(Y,X). p(X,Z) :- q(X,Y), Y=<bob>. becomes p(X,Z) :- q(X,<bob>). p(X,Z) :- q(X,Y), X=Y, Y=<bob>, X=<alice>. throw an Error.

About inequality, we don't have negation in rule bodies (nor in Query in DLGP language), but we have ConjunctiveQueryWithNegatedParts.java in Graal API …

But, what about ? ? :- s(X). with p(a), p(b). as data and

q(X,Y) :- p(X). % Y is existential
s(Y) :- q(X,Y), q(Z, W), Y=W.
s(Y) :- q(X,Y), q(Z, W), Y!=W.

as rules…

[alanruttenberg]

Well, I've stared at your example for a while, but I don't understand it. Could say a few more words?

[sipi]

Hi Alan, Sorry for not replying sooner.

My previous example are not correct to explain the problem because we can deduce that ? :- s(X) is true. Indeed, in a forward chaining (chase) : by q(X,Y) :- p(X). we first deduce : q(a, X0) & q(b, X1) then we can apply s(X) :- q(X,Y), q(Z, W), Y=W. with the following homomorphism : {X->a, Z->a, Y->X0, W->X0} OR {X->b, Z->b, Y->X1, W->X1} (I missed them).

So let me take another simpler example with only inequality :

% query
? :- s(X).

% fact
p(a,b).

% rules
r(X,Z), r(Y,Z) :- p(X,Y). % Z is existential
s(X) :- r(X,Y), X != Y.

So, in a forward chaining (chase), we first obtain :

r(a,Z0), r(b,Z0)

then we can't apply s(X) :- r(X,Y), X != Y. because we can't assert a != Z0 nor b != Z0, so we can't deduce that ? :- s(X) is true.

However, we know that in any logical model of the KB, either Z0 != a is true, or Z0 = a is true. If Z0 != a is true, ? :- s(X) is true. Else Z0 = a, then Z0 != b is true because a != b, and ? :- s(X) is also true.

This shows that rule application is not complete with respect to classical logical entailment as soon as we have inequality atoms that may be mapped to existential variables in the facts (which is our case).

I hope this enlightens you.

[alanruttenberg]

Thank you very much for the response.

I'm being dense and still am having problems understanding. I'll list where I'm confused. Sorry if I've missing some very obvious thing. I hope you understand the below isn't meant to be critical in any way, just a setting out of what I'm not understanding.

• Why do I want to query s(X)? I have vague idea that I should use it when I want inequality, something like if I intended properPart(X,Y) :- Part(X,Y), X!=Y., I write properPart(X,Y) :- Part(X,Y), s(X), s(Y). Is that what is intended?

• The goal is to be able to use inequality, but the rule s(X) :- r(X,Y), X != Y. uses inequality directly, in which case you get inequality in a rule because you already have inequality in a rule.

• In the case analysis, what happens if Z0 != a, and Z0!=b. In that case s(X) is true but it doesn't matter if a=b or a!=b. In the other case, if a=Z0, then I agree we get s(X) only if b!=a, and by symmetry the same if b=Z0. But when Z0 is neither...

• In the first comment you talk about erasing equality. Am I right that this doesn't depend on UNA - that it is generally applicable and so lets you support equality in bodies in general? What UNA seems to add is the ability to throw an exception on a nonsense rule ... :- ... , X=Y, X=<g1>,Y=<g2>.

[ayumi5420467]

Hi sipi, I have tried the EqualityUtils.java you have mentioned in the reply to Alan. Processing query "?(ID,Type) :- class:Investigator(ID,Type),Type = X." gave me the result of "?(ID) :- class:Investigator(ID, X)." My question is, although you could process equality in the rules, how do you reflect the value in the query result?

Thanks