Re: Discussion from today

Dear Doerthe,

Forgot to point to a concrete example
http://ppr.cs.dal.ca:3002/n3/editor/s/IT3znjsL
Here the log: namespace is (mis)used instead of the e: namespace.
Both Cwm and Eye agree again.

Kind regards,
Jos

-- https://josd.github.io


On Tue, Jan 25, 2022 at 11:56 AM Jos De Roo <josderoo@gmail.com> wrote:

> Dear Doerthe,
>
> Agreed and a while ago I did some experiments in which the variables
> in quoted graphs were replaced by either
> (e:existential ?X)
> or
> (e:universal ?X)
> and then using rules like you also suggested to transform that into
> regular data N3 data/rules/queries.
>
> It is also quite close to Pierre-Antoine's proposal of one variable type.
> The scope of those variables is the so-called statement level.
>
> It actually worked quite well.
>
> Kind regards,
> Jos
>
> -- https://josd.github.io
>
>
> On Tue, Jan 25, 2022 at 10:46 AM Doerthe Arndt <
> doerthe.arndt@tu-dresden.de> wrote:
>
>> Dear Jos,
>>
>> I was too fast in the previous mail. There is one example where cwm and
>> Eye differ: http://ppr.cs.dal.ca:3002/n3/editor/s/okGlsqyV
>>
>> But that does not change the message from the previous mail.
>>
>> Kind regards,
>> Dörthe
>>
>>
>> Am 25.01.2022 um 10:38 schrieb Arndt, Dörthe <doerthe.arndt@tu-dresden.de
>> >:
>>
>> Dear Jos,
>>
>> Thank you for sharing. To complete your example, I also added universal
>> quantification: http://ppr.cs.dal.ca:3002/n3/editor/s/IWXT3bhG
>> The reasoners still both do the same.
>>
>> I think that from a logical point of view, some of these derivations are
>> problematic.  But I also better understand, why you would be against fully
>> introducing explicit quantification. That would require us to make a whole
>> theory how reasoning works for the cases mentioned and then to also
>> implement it  accordingly which most likely will never be done since there
>> are not that many use cases which really require that complexity.
>>
>> My proposal was thus more to have some kind of notation for example for
>> proofs with which we can only do further derivation if we express that
>> structure in the rules. Maybe there is a third option between skolem iris
>> and explicit quantification with only minimal support which I am not seeing
>> (yet)?
>>
>> Kind regards
>> Dörthe
>>
>>
>>
>> Am 25.01.2022 um 01:10 schrieb Jos De Roo <josderoo@gmail.com>:
>>
>> Dear Doerthe,
>>
>> I was curious how your 5 examples currently fare with cwm and eye
>> and they both give the same results! Yes, the same results!
>>
>> You can try it at http://ppr.cs.dal.ca:3002/n3/editor/s/tR5T9red
>>
>> So there is a state of the art with explicit quantification and I was
>> not expecting that cwm and eye were so close here.
>>
>> Jos
>>
>> -- https://josd.github.io
>>
>>
>> On Mon, Jan 24, 2022 at 11:21 PM Doerthe Arndt <
>> doerthe.arndt@tu-dresden.de> wrote:
>>
>>> Dear all,
>>>
>>> After our meeting today I thought about explicit quantification and can
>>> say that I actually like the idea to have it in N3 as some kind of
>>> annotation which has no meaning for the reasoning except that it is a kind
>>> of pattern. My vision here is that we would have a  variable namespace
>>> which can be combined with quantifiers. Whenever a cited graph contains a
>>> quantifier, we simply disallow unification with the triples in that graph
>>> unless we also have the quantifier. So, if we come back to my example:
>>>
>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>
>>> { ?y :smurfs { @forSome :X. :X a :Unicorn } } => { ?y a :NaivePerson }.
>>>
>>> Should result in :bob a :NaivePerson. but
>>>
>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>
>>> { ?y :smurfs { _:x a :Unicorn } } => { ?y a :NaivePerson }.
>>>
>>> should not.
>>>
>>> Of course, things could get more complicated here:
>>>
>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>
>>> { ?y :smurfs ?g. ?g log:includes {?x a :Unicorn} } => { ?y a
>>> :NaivePerson }.
>>>
>>> Should not fire, but what about
>>>
>>> :bob :smurfs { @forSome :X. :X a :Unicorn. :Unicorn a :MagicalCreature }.
>>>
>>> { ?y :smurfs ?g. ?g log:includes {?x a :MagicalCreature } } => { ?y a
>>> :NaivePerson }.
>>>
>>> So, here we would have to agree and either decide that the moment that
>>> there is a quantifier involved in the graph, we stay away and do not match
>>> anything, we could use the name-space to know when not to match or we make
>>> a more fine-grained theory about scopes (but here we can really get into
>>> the problems, Jos mentioned). An example:
>>>
>>> :bob :smurfs { @forSome :X. :X a :Unicorn. :X :says {:sokrates a
>>> :Person} }.
>>>
>>> { ?y :smurfs ?g. ?g log:includes {?x :says {:sokrates a :Person} } } =>
>>> { ?y a :NaivePerson }.
>>>
>>> Here, we see that the namspace alone can’t be a reason to allow or
>>> disallow a unification. We would need some concept to express, when a
>>> triple is scoped, and this theory could indeed get complicated.
>>>
>>> (So,I see your concerns here, Jos.)
>>>
>>> So, why do I even propose that kind of pattern? The answer is that I
>>> like that we would have some way to express the patterns which go
>>> beyond our logic which is limited to implicit quantification without
>>> loosing the possibility to involve them to our theory. We could then
>>> explicitly define our reasoning calculus which only allows implicit
>>> quantification and provide rules to support more sophisticated theories. We
>>> cannot express that by only having constants because then there would be no
>>> way of blocking unification.
>>>
>>> My ideas are not really thought through yet (it cn perfectly be that I
>>> change my mind next week, also depending on your comments ;) ). But I
>>> wanted to elaborate why (for now), it seems to be an interesting idea to me.
>>>
>>> Kind regards
>>> Dörthe
>>>
>>
>>
>>