log:notIncludes is order dependant

[pchampin]

More precisely: log:notIncludes behaves differently depending on where the variables in its pattern are bound (similarly to the e:findAll case we discussed during the last meeting).

Example:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .

:alice :name "alice".
:bob :name "bob".
:charlie :name "charlie".

:alice :says { :bob a :NiceGuy }.

@forAll :y.

{ :alice :says ?x.
  :y :name "charlie".
  ?x log:notIncludes { :y a :NiceGuy }.
} => { :test :pass 1 }.

{ :alice :says ?x. 
  ?x log:notIncludes { :y a :NiceGuy }.
  :y :name "charlie".
} => { :test :pass 2 }.

It should produce:

:test :pass 1, 2.

but only test 1 passes.

See http://ppr.cs.dal.ca:3002/n3/editor/s/zfSPYqFV
(but I also tested it locally with the latest commit).

[josd]

Thank you very much @pchampin and this issue should be fixed in https://github.com/josd/eye/releases/tag/v21.1124.2208

@william-vw would you mind to update EYE for http://ppr.cs.dal.ca:3002/n3/editor/s/zfSPYqFV ?

[josd]

While testing further and reading https://pad.lamyne.org/xZF7gcnxTLSNKdueLBYv2A
I realized that there is floundering issue with log:notIncludes and it should be fixed in
the latest EYE version https://github.com/josd/eye/releases/tag/v21.1125.2043

[josd]

So @pchampin for your example

#G1
:gang :contains :bob, :charlie.
:alice :says { :bob :name "bob" }.
{ 
  :alice :says _:g.
  _:g log:notIncludes { _:s _:p _:o }
  :gang :contains _:s.
} => {
  :alice :ignores _:s.
}.

the current version of EYE does not entail

#G2
:alice :ignores :charlie.

anymore, because we now expect the object of log:notIncludes to be ground at reasoning time

[william-vw]

I updated the editor with the latest version of Eye. But I'm unsure whether I agree that the object of log:not Includes should be grounded at reasoning time, or even that the solution to order independence is scoping the variables locally.. At least for me this would break several use cases that rely on a quoted graph (or, current document) not to include certain properties of an identified resource, e.g., ``` ?composite a :CompositeTask ; <> log:notIncludes { ?composite :subTask ?sub } . ``` I know something similar can be achieved with collectAllIn (a.k.a. findall) but this is a much less verbose solution IMO, and I'm unclear why it shouldn't be allowed.

…

________________________________ From: Jos De Roo ***@***.***> Sent: Thursday, November 25, 2021, 4:56 p.m. To: josd/eye Cc: William Van Woensel; Mention Subject: Re: [josd/eye] log:notIncludes is order dependant (Issue #25) So @pchampin<https://github.com/pchampin> for your example #G1 :gang :contains :bob, :charlie. :alice :says { :bob :name "bob" }. { :alice :says _:g. _:g log:notIncludes { _:s _:p _:o } :gang :contains _:s. } => { :alice :ignores _:s. }. the current version of EYE dor not entail #G2 :alice :ignores :charlie. anymore, because we now expect the object of log:notIncludes to be ground at reasoning time — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub<#25 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AC2PLMHFIO7DYMVFLG3FYADUN2PGBANCNFSM5IVQEROQ>. Triage notifications on the go with GitHub Mobile for iOS<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[josd]

The grounding was to avoid an inconsistency i.e. for

#G1
:gang :contains :bob, :charlie.
:alice :says { :bob :name "bob" }.
{ 
  :alice :says _:g.
  _:g log:notIncludes { _:s _:p _:o }
  :gang :contains _:s.
} => {
  :alice :ignores _:s.
}.

we got it that both
_:g log:notIncludes { :bob _:p _:o }
and
_:g log:includes { :bob _:p _:o }
were the case.

[pchampin]

On 26/11/2021 17:29, Jos De Roo wrote: The grounding was to avoid an inconsistency i.e. for |#G1 :gang :contains :bob, :charlie. :alice :says { :bob :name "bob" }. { :alice :says _:g. _:g log:notIncludes { _:s _:p _:o } :gang :contains _:s. } => { :alice :ignores _:s. }. |

Just to be clear: I am not all sure that this example should work as it is. We are in unchartered territory here, with only one kind of variable... Like William, I don't like the idea that the "argument" of log:notIncludes should be entierly ground. Consider the adaptation of the example above that is working for CWM: :gang :contains :bob, :charlie. :alice :says { :bob :name "bob" }. @forall :g, :s. { :alice :says :g. :g log:notIncludes { :s _:p _:o }. :gang :contains :s. } => { :alice :ignores :s. }. http://ppr.cs.dal.ca:3002/n3/editor/s/KFAEqJIB That makes a lot of sense to me. I would like to keep this.

we got it that both |_:g log:notIncludes { :bob _:p _:o }| and |_:g log:includes { :bob _:p _:o }| were the case.

It does not have to be. I would consider that only the second should stand... See a more complete example working with CWM: http://ppr.cs.dal.ca:3002/n3/editor/s/3PlFXPry   pa

…

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#25 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACKLZCP5WXBHLOIYVMIQ7DUN6YXDANCNFSM5IVQEROQ>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[josd]

I thought I wanted that too but then you came up with this issue and the only way I found (after 3 days of trying)
was to use NAF and in Prolog this only works when negated goal is ground i.e.

From The Art of Prolog 1st ed. (Leon S. Sterling, Ehud Y. Shapiro, 1986), p. 166:

The implementation of negation as failure using the cut-fail combination does not work correctly for nonground goals (...). In most standard implementations of Prolog, it is the responsibility of the programmer to ensure that negated goals are grounded before they are solved. This can be done either by a static analysis of the program, or by a runtime heck, using the predicate ground (...)

The line in question in our current code is https://github.com/josd/eye/blob/cdf168e6c644a73d20f47087f614597f46794176/eye.pl#L5340

[doerthe]

Today, I had a meeting with a colleague of mine who pointed out that there is a general problem if you combine negation with existential rules.

If your notion of "ground" allows you to unify a variable which is used in log:notIncludes with a blank node which is produced by a rule, you still have order dependency (this time it is the order of your rules which causes problems).

As an example consider the following:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <www.example.org#> .

:bob a :Person.
:bob :father :ted.

{?x a :Person}=>{?x :father _:y. _:y a :Man}.
{?x :father ?y. ?x :father ?z.  ({?x :father ?y. ?x :father ?z.}) log:conjunction ?u}=>{:my :graph ?u}.
{ :bob :father ?y. :bob :father ?z. :my :graph ?u. ?u log:notIncludes {:bob :father ?y. :bob :father ?z.} }=>{:o :o :o}.

{?x :father ?y}=>{?y a :Man}.

With that you will derive the triple :o :o :o. (see: link)

But if you change the order of the rules here and write the first rule later like here:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <www.example.org#> .

:bob a :Person.
:bob :father :ted.


{?x :father ?y. ?x :father ?z.  ({?x :father ?y. ?x :father ?z.}) log:conjunction ?u}=>{:my :graph ?u}.
{ :bob :father ?y. :bob :father ?z. :my :graph ?u. ?u log:notIncludes {:bob :father ?y. :bob :father ?z.} }=>{:o :o :o}.

{?x :father ?y}=>{?y a :Man}.
{?x a :Person}=>{?x :father _:y. _:y a :Man}.

The triple :o :o :o. will not be derived (see: here).

The reason of for that is the chase the EYE reasoner uses, that is the strategy to (not) apply existential rules. In the first example, the rule

{?x a :Person}=>{?x :father _:y. _:y a :Man}.

applied to :bob a :Person. leads to new information: Bob does not only have a father (Ted), he also has a father of which we know that he is male (but in that situation we do not know whether that father is actually Ted or not), later we also derive with the vary last rule that Ted is also male.

If we change the position of that last rule which gives us the information that Ted is male to a position before the rule

{?x a :Person}=>{?x :father _:y. _:y a :Man}.

that rule will not fire since we already have an instance for the new existential in the head of the rule. If we know that

:bob :father :ted.
:ted a :Man.

there is no information gained by constructing

:bob :father [ a :Man].

We can construct similar examples with other built-ins which mimic some kind of negation, for example:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <www.example.org#> .

:bob a :Person.
:bob :father :ted.

{?x :father ?y}=>{?y a :Man}.
{?x a :Person}=>{?x :father _:y. _:y a :Man}.
{?x :father ?y. ?x :father ?z. ?y log:notEqualTo ?z}=>{:here :I :am}.

Does NOT produce :here :I :am. while

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <www.example.org#> .

:bob a :Person.
:bob :father :ted.

{?x a :Person}=>{?x :father _:y. _:y a :Man}.
{?x :father ?y. ?x :father ?z. ?y log:notEqualTo ?z}=>{:here :I :am}.
{?x :father ?y}=>{?y a :Man}.

does produce :here :I :am. (see: example1 vs. example2 ).

He did not (yet?) have a solution for the problem except the rather big restriction that we do not only expect the triples in a negation to be bound but also that the are not bound to variables which are produced using an existential rule.

I would like to know your thoughts about that.

[josd]

With that you will derive the triple :o :o :o. (see: link)

This is no longer the case in the latest EYE release https://github.com/josd/eye/releases/tag/v21.1203.1050

I have collected all the tests for this issue at https://github.com/josd/eye/tree/master/reasoning/issue25

So at this moment the alien triples :o :o :o. and :here :I :am. are no longer produced but it still feels like
more will be needed ...

[doerthe]

The person who told me just wrote a whole paper about the issue. The solution in the paper is to always reduce the model you produce via the rules towards a core model before you apply negation, but in my opinion that is too expensive to do in practice

[doerthe]

This is no longer the case in the latest EYE release https://github.com/josd/eye/releases/tag/v21.1203.1050

Maybe also mention Stephan Mennicke as the observer of the problem (he pointed me to the general problem of existentials and negation :) )

[josd]

Very well, and Stephan is now mentioned in the latest release https://github.com/josd/eye/releases/tag/v21.1203.1426

[doerthe]

Here the paper about that issue: https://arxiv.org/pdf/2112.07376.pdf
Maybe we can use some of the ideas discussed there.