Re: Hello, n3

Dear Nathan, all,

Thank you for pushing this forward!  I am really happy that you are as 
enthusiastic about this topic as I am. I always wanted to push forward 
the formalisation of N3, so I guess, now is the time.

A little bit more about my and our background:

I have a master in Mathematics and I am currently finishing my PhD in 
Computer Science which has N3 and its applications as a topic. I work at 
imec in Gent (Belgium) and there, we had many research projects using N3 
and the EYE reasoner (I am sure Jos will tell us more about his 
implementation in another mail, till then you can already check 
http://eulersharp.sourceforge.net/ and http://n3.restdesc.org/).

Some example projects :

  * We implemented owl-rl rules in N3 and used it for ontology reasoning
    (maybe an idea to also test it on the work of you, William, but that
    is just a side note :) ). What was special about N3 here was that N3
    allows rules in the consequence of rules ( like {?C1
    rdfs:subClassOf  ?C2}=>{ {?x a ?C1}=>{?x a ?C2} }.). We used this
    for preprocessing. [1]

  * We also had several projects in which we used the fact that Cwm and
    EYE both can produce proofs. We created a format to describe
    possible restful Web API calls in forms of rules with existential
    variables in the consequence (another nice feature of N3), RESTdesc.
    The user can then give a goal he or she wants to reach and by
    producing a proof the computer provides a plan  how this goal can be
    reached. [2,2a]

  * We used N3 for data validation. Here, we used a lot of the built-ins
    of N3, but also  the RIF built-ins as they are implemented in EYE. [3]

We also already worked on the formalisation of N3 and identified several 
problems which need to be fixed:

  * *Implicit quantification:* When we used the reasoners Cwm and EYE,
    we discovered, that they differed in their way of handling implicit
    universal quantification. To give a concrete example, consider the rule:

        {{?x :p :o} => {?x :p2 :o2}}=> {:a :b :c}.

    Cwm interprets that as:

        (∀x: p(x,o) → p2(x,o2)) → b(a,c)

    EYE interprets it as:

        ∀x: (p(x,o) → p2(x,o2)) → b(a,c)

    The reason for that the W3C team submission is not really clear
    here, it says that universals are quantified "on the parent formula"
    (see https://www.w3.org/TeamSubmission/n3/#Quantifica), but it does
    not say what exactly this "parent" is.

  * *Explicit quantification: *N3 provides a way to express explicit
    quantification (by using @forall and @forsome). An example formula is:

      @forAll <#h>. @forSome <#g>. <#g> <#loves> <#h> .

    which means in FOL:

    ∀h: ∃g: loves(h,g)

    But the spec also says that /"If both universal and existential
    quantification are specified for the same formula, then the scope of
    the universal quantification is outside the scope of the
    existentials" /(see
    https://www.w3.org/TeamSubmission/n3/#Quantifica). So the formula

    @forSome <#g>. @forAll <#h>. <#g> <#loves> <#h> .

    also means

    ∀h: ∃g: loves(h,g)

    I at least think that this is counter intuitive (but maybe there are
    good reasons to do it that way?).

  * *No distinction between variables and constants:

    *Related to the previous topic, it can be a problem that variables
    and constants are not clearly distinguished. Look for example at the
    first occurence of :h in this formula:

    @forSome :g. :g :p *:h*.  @forAll :h. :g :loves :h .

    Given the reversal of quantifiers when interpreting it (∀h: ∃g: ...)
    it is not clear to me whether this :h is a universally quantified
    variable or a constant.


  * *Citation of Formulas:
    *We need to agree how to interpret cited graphs like for example

    :x :says {:s :p :o}.

    I think this topic is quite challenging (for TriG, for example,
    there was no agreement https://www.w3.org/TR/rdf11-datasets/). RDF*
    [4] reduces such constructs to rdf reification which unfortunately
    doesn't solve the problem of defining a semantics since reification
    is excluded in rdf semantics (see:
    https://www.w3.org/TR/rdf11-mt/#reification). There are many
    different approaches we could follow like for example KIF [5],
    Common Logic [6] or also make it more complex like they do in SUMO [7].

I worked on the quantification part and published a paper in 2015 about 
that [8] (it is only a first draft which especially does not yet take 
the position of a quantifier into account) begin our discussions, till 
then I can refer to my presentation about this topic here: 
https://docs.google.com/presentation/d/1Tkh3JLuayBft63ltoeCCD68Zfa9wMFzjOz-h_xYX0PU/edit?usp=sharing 
(I enabled commenting in case you want to ask questions). I furthermore 
also did some work on formalising the proof calculus for N3, this part 
can be found in our Paper Pragmatic Proof [2a].

As you see. I am really interested in writing the spec, but I am also 
willing to invest time in working on and testing implementation(s) and I 
am looking forward to having detailed discussions.

I am looking forward to working with you.

Kind regards,
Dörthe



[1]  D. Arndt, B. De Meester, P. Bonte, J. Schaballie, J. Bhatti, W. 
Dereuddre, R. Verborgh, F. Ongenae, F. De Turck, R. Van deWalle, E. 
Mannens, Improving OWL RL reasoning in N3 by using specialized rules, 
in: V. Tamma, M. Dragoni, R. Gonçalves, A. Ławrynowicz (Eds.), Ontology 
Engineering: 12th International Experiences and Directions Workshop on 
OWL, Vol. 9557 of Lecture Notes in Computer Science, Springer, 2016, pp. 
93–104. doi:10.1007/978-3-319-33245-1_10. URL 
http://dx.doi.org/10.1007/978-3-319-33245-1_10

[2] http://restdesc.org/

[2a] R. Verborgh, D. Arndt, S. Van Hoecke, J. De Roo, G. Mels, T. 
Steiner, J. Gabarró Vallés, The pragmatic proof: Hypermedia API 
composition and execution, Theory and Practice of Logic Programming 17 
(1) (2017) 1–48. doi:10.1017/S1471068416000016. URL 
http://arxiv.org/pdf/1512.07780v1.pdf

[3] D. Arndt, B. De Meester, A. Dimou, R. Verborgh, E. Mannens, Using 
rule-based reasoning for RDF validation, in: S. Costantini, E. Franconi, 
W. Van Woensel, R. Kontchakov, F. Sadri,
D. Roman (Eds.), Proceedings of the International Joint Conference on 
Rules and Reasoning, Vol. 10364 of Lecture Notes in Computer Science, 
Springer, 2017, pp. 22–36. doi:10.1007/978-3-319-61252-2_3. Available 
at: https://biblio.ugent.be/publication/8540876/file/8540882.pdf

[4] O. Hartig, B. Thompson, Foundations of an alternative approach to 
reification in RDF, CoRR abs/1406.3399. arXiv:1406.3399. URL 
http://arxiv.org/abs/1406.3399

[5] P. Hayes, C. Menzel, A semantics for the knowledge interchange 
format, in: IJCAI 2001 Workshop on the IEEE Standard Upper Ontology, 
Vol. 1, 2001, p. 145.

[6] ISO/IEC 24707:2007 Information technology – Common Logic (CL), 
standards.iso.org/ittf/PubliclyAvailableStandards/c039175_ISO_IEC_24707_2007%28E%29.zip 
(2007).

[7] C. Benzmüller, A. Pease, Higher-order aspects and context in sumo, 
Web Semantics: Science, Services and Agents on the World Wide Web 12 
(2012) 104–117.

[8] D. Arndt, R. Verborgh, J. De Roo, H. Sun, E. Mannens, R. Van de 
Walle, Semantics of Notation3 logic: A solution for implicit 
quantification, in: N. Bassiliades, G. Gottlob,F. Sadri, A. Paschke, D. 
Roman (Eds.), Rule Technologies: Foundations, Tools, and Applications, 
Vol. 9202 of Lecture Notes in Computer Science, Springer, 2015, pp. 
127–143. URL http://link.springer.com/chapter/10.1007/978-3-319-21542-6_9

> Hi all, thanks for joining the n3-dev CG.
>
> Since the holiday season is fast approaching, we should perhaps aim to 
> start ramping up communications and efforts from the new year.
>
> If you know anybody else who may be interested in joining, or should 
> be involved, please encourage them to join the CG via 
> https://www.w3.org/community/n3-dev/
>
> In the interim, please do share anything you think is pertinent, 
> including related background reading and references, or anything you'd 
> like to discuss. It may also be useful to start collating 
> implementations, any nuances or bugs that have been found after 
> working with the current specification [1] (see also [2]), also 
> suggestions on what could be improved / simplified / expanded / removed.
>
> Let's all get on the same page, agree what to do, and get it done.
>
> Personally I'll commit time, discussion, spec writing, mistakes, and 
> working reference implementation(s). Throughout the current decade 
> I've frequently thought or said I/you/we could do this with n3, so 
> before the turn of the next decade, /I want/ to be using n3+rules 
> daily, at scale, and will do my utmost to facilitate you all in using 
> it for what you want or need too.
>
> Thanks all, and I look forward to working you all in the coming months,
>
> Nathan
>
> [1] https://www.w3.org/TeamSubmission/n3/
> [2] https://www.w3.org/DesignIssues/Notation3.html

-- 
Dörthe Arndt
Researcher Semantic Web
imec - Ghent University - IDLab | Faculty of Engineering and Architecture | Department of Electronics and Information Systems
Technologiepark-Zwijnaarde 19, 9052 Ghent, Belgium
t: +32 9 331 49 59 | e:doerthe.arndt@ugent.be