Discussion from today

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