Re: Discussion from today

Dear Doerthe,

To deal with both log:universal and log:existential we can simply use
nested log:scope like in the example
http://ppr.cs.dal.ca:3002/n3/editor/s/1Jisg9ES

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

:bob :smurfs {
    (log:universal :a) log:scope {
        (log:existential :x :u) log:scope {
            :x a :Unicorn.
            :u :p :x.
        }.
        :a :p :o.
    }
}.

{
    ?y :smurfs {
        (log:universal :b) log:scope {
            :b :p :o.
            (log:existential :v :y) log:scope {
                :v :p :y.
                :y a :Unicorn.
            }
        }
    }
} => {
    ?y a :NaivePerson.
}.

Using the latest eye
<https://github.com/josd/eye/releases/tag/v22.0126.1149> it can derive

:bob a :NaivePerson.

Kind regards,
Jos

-- https://josd.github.io


On Tue, Jan 25, 2022 at 4:07 PM Jos De Roo <josderoo@gmail.com> wrote:

> 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
>>>>>
>>>>
>>>>
>>>>
>>