Formalisation of N3

Next Topic
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view

Formalisation of N3

Dörthe Arndt-2
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: (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:

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.

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 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: [hidden email]