Re: Discussion from today

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
>