Re: FW: Discussion on log:notIncludes

Was declaring victory for http://ppr.cs.dal.ca:3002/n3/editor/s/0HrLHpgS too
early ..
There is still an issue with premis order dependency  as none of the
following gives an answer:

{?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?x a :task. ?ys
log:equalTo ().} => { ?x :empty1 :true }.
{?Scope e:find (?task {?x :subTask ?task.} ?ys). ?x a :task. ?ys
log:equalTo ().} => { ?x :empty2 :true }.
{(?task {?x :subTask ?task.} ?ys) log:collectAllIn ?Scope. ?x a :task. ?ys
log:equalTo ().} => { ?x :empty3 :true }.

{?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?ys log:equalTo (). ?x
a :task.} => { ?x :empty1 :true }.
{?Scope e:find (?task {?x :subTask ?task.} ?ys). ?ys log:equalTo (). ?x a
:task.} => { ?x :empty2 :true }.
{(?task {?x :subTask ?task.} ?ys) log:collectAllIn ?Scope. ?ys log:equalTo
(). ?x a :task.} => { ?x :empty3 :true }.

{?ys log:equalTo (). ?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?x
a :task.} => { ?x :empty1 :true }.
{?ys log:equalTo (). ?Scope e:find (?task {?x :subTask ?task.} ?ys). ?x a
:task.} => { ?x :empty2 :true }.
{?ys log:equalTo (). (?task {?x :subTask ?task.} ?ys) log:collectAllIn
?Scope. ?x a :task.} => { ?x :empty3 :true }.

For the moment I see only one solution which is with log:notIncludes and
bind all the variables in its object
via extra :subTask declarations like in
http://ppr.cs.dal.ca:3002/n3/editor/s/fCR2HSVh
That gives the expected answer
:cmp1 :empty :true.

Kind regards,
Jos

-- https://josd.github.io


On Mon, Dec 13, 2021 at 8:15 PM Jos De Roo <josderoo@gmail.com> wrote:

> Doerthe was testing alternative SNAF ways in
> http://ppr.cs.dal.ca:3002/n3/editor/s/0HrLHpgS
> but there is an issue with e:find which is now solved in
> https://github.com/josd/eye/releases/tag/v21.1213.1906
> So if William could do an upgrade, the results should then be
>
> :cmp1 :empty1 :true.
> :cmp1 :empty2 :true.
> :cmp1 :empty3 :true.
> :cmp1 :empty4 :true.
> :cmp1 :empty5 :true.
> :cmp1 :empty6 :true.
>
> Kind regards,
> Jos
>
> -- https://josd.github.io
>
>
> On Mon, Dec 13, 2021 at 6:12 PM William Van Woensel <
> william.vanwoensel@gmail.com> wrote:
>
>> Dear mailing list,
>>
>>
>>
>> Below you can find a conversation on log:notIncludes that may be of
>> interest!
>>
>>
>>
>>
>>
>> Regards,
>>
>>
>>
>> William
>>
>>
>>
>> *From: *Doerthe Arndt <doerthe.arndt@tu-dresden.de>
>> *Date: *Monday, December 13, 2021 at 9:29 AM
>> *To: *William Van Woensel <william.vanwoensel@gmail.com>
>> *Cc: *Jos De Roo <josderoo@gmail.com>, Pierre-Antoine Champin <
>> pierre-antoine.champin@ercim.eu>, Gregg Kellogg <gregg@greggkellogg.net>
>> *Subject: *Re: Discussion on log:notIncludes
>>
>> Dear William,
>>
>>
>>
>> Sorry for my late answer. I agree with your explanation and I also think
>> that the main question is: what does the local scoping of variables mean?
>> Related to that, it is also important to know where exactly our negation is
>> (so we have „implicit negation :) ).
>>
>>
>>
>>
>>
>> To come to your examples
>>
>>
>>
>>
>>
>> To continue our discussion on log:notIncludes (and in general the
>> floundering issue) I found a good link yesterday:
>> https://github.com/dtonhofer/prolog_notes/blob/master/other_notes/about_negation/floundering.md
>>
>>
>>
>> I was wondering why my particular example made sense, but the one in the
>> above article does not, even when *not* exposing variables outside of the
>> “notIncludes” statement.
>>
>>
>>
>> Starting from the beginning, the following doesn’t make sense much sense
>> because of floundering (as mentioned in the article):
>>
>>
>>
>> :bart :allergicTo :penicillin .
>>
>>
>>
>> { <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :canTake ?y }
>> . # no
>>
>> { <> log:notIncludes { :bart :allergicTo :eyrthromycin } } => { :bart
>> :canTake :eyrthromycin } . # yes (contradiction; above rule did not output
>> anything, meaning that bart cannot take anything)
>>
>> { <> log:notIncludes { :lisa :allergicTo ?y } } => { :lisa :canTake ?y }
>> . # yes, but don't know what to bind to y
>>
>>
>>
>> (there is much more in the article, such as possible general solutions to
>> this problem)
>>
>>
>>
>> This actually made clear to me why having “builtin-local” variables,
>> i.e., not exposing “y” to the rule consequent, could be a solution to the
>> problem, as they would at least prevent these use cases. I believe this was
>> implied during our last discussion but I hadn’t gotten that far yet :-)
>>
>> The examples here seems to assume that the variable here is universally
>> quantified on top level.
>>
>>
>>
>>
>>
>>
>>
>> The problem is indeed, that if we wanted the rule to work as it might was
>> intended by its inventor, we would have to list everything which :bart can
>> take which would be everything (in the world) except :penicillin. We can’t
>> list everything except penicillin.
>>
>>
>>
>> In the last rule we have the same, but here, there is no exception. We
>> can state :lisa :canTake ?y., if we allow universal variables on top
>> level and have some shorthand for „Lisa can take everything“.
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> However, if we slightly re-write these examples to not expose any
>> builtin-local variables:
>>
>>
>>
>> :bart :allergicTo :penicillin .
>>
>>
>>
>> { <> log:notIncludes { :bart :allergicTo ?y } } => { :bart
>> :canTakeSomeDrug true } . # still no
>>
>> { <> log:notIncludes { :lisa :allergicTo ?y } } => { :lisa
>> :canTakeSomeDrug true } # still yes
>>
>>
>>
>> This still doesn’t make much sense to me – due to the intuition that,
>> just because bart has an allergy to one particular drug, it doesn’t mean
>> they cannot take some other drug. (This is similar to the first statement
>> in the first example: just because bart has an allergy to one particular
>> drug, it doesn’t mean they cannot take some other drug.)
>>
>> Here, it depends on the meaning you assume for the universal. If you are
>> consistent with the example above, you would still have universal scoping
>> on top level. So, what you say here would be in FOL:
>>
>>
>>
>> \forall y: (\not allegicTo(bart,y))-> canTakeSomeDrug(bart, true).
>>
>>
>>
>> Which means the same as:
>>
>>
>>
>> (*\exists y: \not (*allegicTo(bart,y)))-> canTakeSomeDrug(bart, true).
>>
>>
>>
>> In that interpretation, the rule makes sense.
>>
>>
>>
>> What you describe (and what is also implemented) is different. From your
>> lines above I see that you understand the rule as:
>>
>>
>>
>> (* \not (\exists y: *allegicTo(bart,y)))-> canTakeSomeDrug(bart, true).
>>
>>
>>
>> With that interpretation, the rule does not make sense, but the behavior
>> of the reasoner does.
>>
>>
>>
>>
>>
>> Now, compare with my use case:
>>
>>
>>
>> :cmp0 :subTask :s0 .
>>
>>
>>
>> { <> log:notIncludes { :cmp0 :subTask ?y } } => { :cmp0 :empty :true } .
>> # no (e.g., “cmp0” could have been bound in an earlier triple)
>>
>> { <> log:notIncludes { :cmp1 :subTask ?y } } => { :cmp1 :empty :true } .
>> # yes (idem)
>>
>>
>>
>> Here, the mere mentioning of a composite task with the property “subTask"
>> *indeed means* that it is not empty. Having one subtask means something is
>> not empty (counter-example).
>>
>>
>>
>>
>>
>> I can again translate.
>>
>>
>>
>> The rule you want to express is:
>>
>> (* \not (\exists y: *subTask(cmp0,y)))-> isEmpty(cmp0, true).
>>
>>
>>
>> What we would get if we had the y quantified on top level would be:
>>
>>
>>
>> *\forall y: *( *  \not (*subTask(cmp0,y)))-> isEmpty(cmp0, true).
>>
>>
>>
>> which can be transformed to:
>>
>>
>>
>> ( *\exists y:  \not (*subTask(cmp0,y)))-> isEmpty(cmp0, true).
>>
>>
>>
>> But, in the drug example, the mere mentioning of a person with property
>> “allergicTo” property *does not mean* that they cannot take something.
>> Having one drug allergy does not mean one cannot take some (other) drug
>> (not a counter-example).
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> So it is related to the meaning we assign to the inference. E.g., the
>> following would make much more sense:
>>
>>
>>
>> { <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :hasAllergies
>> false } . # still no, but this is good
>>
>>
>>
>> Or
>>
>>
>>
>> { <> log:notIncludes { :bart :allergicTo ?y } } => { :bart
>> :canTakeAnyDrug true } . # still no, but this is good
>>
>>
>>
>>
>>
>> Hence I feel that the second drug example (“canTakeSomeDrug”) is rather
>> an anti-pattern, as it does not search for the non-existence of a
>> counter-example – this could be mentioned in the N3 spec (yes remember that
>> thing? >:). Could this, combined with a “builtin-local” scoping of the
>> variables, be a solution for the notIncludes problem? (Sorry if some of you
>> may have already gotten to this point – I just needed a bit more exposition)
>>
>>
>>
>>
>>
>>
>>
>> As I pointed out above with the examples. I think that the examples of
>> negation where we have „floundering“ are actually cases where the universal
>> quantification which is supposed to be on top-level suddenly switched to a
>> local level. This is something which should not happen and therefore, I
>> agree with Jos that we should be very strict here.
>>
>>
>>
>> I also see, that the use of negated predicates as you describe them has
>> many use cases and I know that I did similar things before (but with
>> e:findAll, where it is easier to understand the variable as locally
>> quantified). So, I would suggest, that we go for some kind of local
>> variable here.
>>
>>
>>
>> We could for example use blank nodes in that context and use their
>> specification as it was in the original proposal. There, they are local.
>>
>>
>>
>> It even works if they are existential quantified. In that case, it still
>> depends on the position of the implicit negation, whether or not we get the
>> meaning you intended in your example. But if we say that the existential
>> quantifier comes before the negation, then your example would work.
>>
>>
>>
>> It is interesting to see that this is also how cwm sees it. With the
>> original meaning of blank nodes (so no re-interpretation), your example
>> works. You can see that in Cwm:
>> http://ppr.cs.dal.ca:3002/n3/editor/s/yRnwKhdK
>>
>>
>>
>> Kind regards,
>>
>> Dörthe
>>
>>
>>
>>
>>
>>
>>
>