Re: Discussion from today

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<mailto: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<mailto: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<https://josd.github.io/>


On Mon, Jan 24, 2022 at 11:21 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto: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