Re: Discussion from today

Dear Doerthe,

Your log:scope is an excellent proposal and I was able to extend unify/2
in the latest eye https://github.com/josd/eye/releases/tag/v22.0125.1445
so that http://ppr.cs.dal.ca:3002/n3/editor/s/SHY7RXbG should give
:bob a :NaivePerson1 but not :bob a :NaivePerson1
of course after that @William Van Woensel <William.Van.Woensel@dal.ca>
resolves
https://github.com/william-vw/n3-editor-js/issues/5

Kind regards,
Jos

-- https://josd.github.io


On Tue, Jan 25, 2022 at 1:29 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de>
wrote:

> Dear Jos,
>
> That is very interesting and I like the compact notion. I am not sure
> about the use of the universal, but that is a separate discussion.  I
>  still have two bigger concerns:
>
> 1. We can only quantify over triples and not over formulas which is what
> we would actually need.
> 2. The quoted variable could still be seen as a constant, look for example
> here: http://ppr.cs.dal.ca:3002/n3/editor/s/ioYMxfcC
>
> So we could do something like :bob :smurfs { (log:existential :x)
> log:scope {:x a :Unicorn.} }.
>
> This looks far less elegant than your solution but we have the advantage
> that the scope is clearly defined and that we can quantifiy over formulas.
> Maybe you have an idea ho to improve that?
>
> Kind regards,
> Dörthe
>
> Am 25.01.2022 um 12:20 schrieb Jos De Roo <josderoo@gmail.com>:
>
> 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
>>>>
>>>
>>>
>>>
>