Formalisation of N3

Dear Dan,

as you proposed, I included public-cwm-talk to our conversation.

To help anyone else who is reading this mail: we are discussing about 
the following paper: 
http://link.springer.com/chapter/10.1007/978-3-319-21542-6_9 (please 
send me an E-mail if you are interested and cannot access it). It 
proposes a formalisation of N3 and was meant to raise the discussion 
especially on quantification in N3. So feedback is more than welcome!

> The paper was quite interesting, overall. The "use of a substitution 
> function which maps into the set ground- and ungroundable expressions 
> instead of a classical valuation function mapping directly into the 
> domain of discourse" is the interesting bit.

We thought a lot about especially that part.  One reason we did this 
restriction was that we were afraid to end up in higher order logic if 
we'd allow quantifying directly over predicates (= sets of pairs).

>
> I haven't carefully considered the impact of the proposal:
>
>   We see all these as reasons to propose a change in the 
> specification: the scope of a universally quantified variable should 
> be the whole formula it occurs in and not just a nested sub-formula.
>
An nice example for the different implementations can be seen here: 
https://lists.w3.org/Archives/Public/public-cwm-talk/2015JanMar/0003.html

Additionally to this and the rule example of the paper,  implicit 
universal quantification would not even be able to produce what we 
called ungroundable expressions.

ClarkKent believes {Lois believes { ?a a Hero }}

Superman a Hero
Batman a Hero

Would not mean any more that /"Clark Kent believes that Lois believes 
that everyone is a hero"/, but  that /"Clark Kent believes that Lois 
believes that Superman is a hero" /and /"Clark Kent believes that Lois 
believes that Batman is a hero"
/(and strictly speaking also in//"Clark Kent believes that Lois believes 
that ClarkKent is a hero"// or even////"Clark Kent believes that Lois 
believes that believes is a hero", ////but that is 
another////////story).////
////

////////
In this context it is also worth to mention, that the scope of 
existentials is equally interesting:

_:x believes { _:x a Hero }

In EYE this would mean

\exists x: x believes (x a hero)


In cwm

\exists x1: x1 believes (\exists x2: x2 a hero).


But maybe it is best to first come to solution for universal 
quantification before opening this new discussion.

> I suppose EYE implements this proposal; has it been run over the cwm 
> test suite? surely it has. Does the difference show up in any test cases?
I'd like to forward this question to Jos, but I doubt that the test 
suite contains that kind of examples?

>
> I'm in favor of more straightforward formalization for N3, but I 
> puzzled over it for years and became quite doubtful that there's any 
> sane way to formalize it. I kept trying combinations of substitution 
> functions and valuation functions, but I could never get the superman 
> case to work out.
> https://lists.w3.org/Archives/Public/public-cwm-talk/2005AprJun/0000.html
>
For me it is really interesting to see that the discussion about 
quantification is not new at all.

I am still not sure what to do with the graph constructions:
How would you understand a quoted graph containing a variable? Should it 
map to one or several elements of the universe of discourse? As it is 
much easier to formalise, I chose the first option, but maybe there are 
arguments for the second one?


> The real challenge is log:includes, as you say...
>
>    In the first publication about Notation3 Logic [7] the most complex 
> of those predicates were, among others, log:includes, log:notIncludes 
> and log:semantics. We consider a careful examination of those 
> predicates important.
>
I didn't dare to touch it yet, but it would indeed be the next step.

> p.s. I'm inclined to copy public-cwm-talk on this conversation. Do you 
> mind?
>
I think it is a great idea, see above.

Thank you for your comments!
Best regards,
Dörthe



-- 
Dörthe Arndt
Researcher Semantic Web
Ghent University - iMinds - Data Science Lab
Faculty of Engineering and Architecture
Department of Electronics and Information Systems
Sint-Pietersnieuwstraat 41, 9000 Ghent, Belgium

t: +32 9 331 49 59
e: doerthe.arndt@ugent.be
URL:  http://datasciencelab.ugent.be/