Re: Discussion from today

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