Re: Implicit Quantification in N3

On 2015-01 -16, at 11:05, Dörthe Arndt <dorthe.arndt@ugent.be> wrote:

> Hello,
> 
> I am currently trying to write down the basic formal semantics of N3 and I had some problems with implicit quantification. Maybe you could help me here?
> 
> I am not 100% sure how the scope of the universal quantifiers is. If I have for example the formula:

They are universally quantified in the graph one outside the one they are mentioned in.  This is to 
get simple rules to work like sparql.
 
> 
>    {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.
> 
> Are the four ?x the same?

No, the first two are the same and the second two are.

If in doubt use @forAll 


> Does it mean
> 
>    1. ∀x: ((p(x,o) → pp(x,o))→(g(x,l)→k(x,o)))
> 
> or
> 
>    2. ((∀x_1 p(x_1, o) → pp(x_1, o))→(∀x_2 g(x_2, l)→k(x_2, o)))

The latter

> 
> 
> I checked in the N3 team submission (http://www.w3.org/TeamSubmission/N3/#Quantifica) which states:
> 
> "Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quanitified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula"


The important bit here is 'not in the formula but in its parent formula'.



> 
> This and the behaviour of the cwm reasoner (http://www.w3.org/2000/10/swap/doc/cwm.html) in that case, suggest that it is 2. But in the EYE reasoner (http://eulersharp.sourceforge.net/) the first option seems to be implemented (and this first interpretation would also be easier to formalise).
> 

I wasn't aware that EYE was different.

The reason for having the rule that the quantification is in the parent formula is that 

1) that makes it work as you would expect with simple rules


 { ?x :p ?y  } => { ?y :p ?x }.


2) If you can and paste a rule into something else, it doesn't change it meaning

@forAll :p.

 { :p a  :SymmetricProperty } =>  {{ ?x :p ?y  } => { ?y :p ?x }}.

works.  But note you cannot use ?p -- you have to explicitly quantify p.

I hope this helps.


> What about nested formulas? Is the quantification on top level inherited or is there a new quantifier for every level? For EYE it is inherited, but I tested two examples in cwm:
> 
>    1. {?y :p :o}=> {:s :p {?y :pp :o}}.
> 
>    2. {:s :p :o}=> {?x :p {?x :pp :o}}.
> 
> According to its parsing, the ?y in the first formula are the same, the two ?x of the second formula aren't.



> cwm's interpretation:
> 
>    1.  ∀y: (p(y,o) → p(s,pp(y,o))
> 
>    2. p(s,o) → (∀x_1: p(x_1,(∀x_2: pp(x_2,o))
> 
> So, how is it supposed to be? Maybe I am misunderstanding it, but shouldn't the parsing for the two formulas behave similarly?
> Why is there a difference?
> 
> Thank you in advance for your help!
> 
> Kind regards,
> Dörthe Arndt
> 
> -- 
> Dörthe Arndt
> Researcher Semantic Web
> Ghent University - iMinds - Multimedia Lab
> Faculty of Engineering and Architecture
> Department of Electronics and Information Systems
> Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium
> 
> t: +32 9 331 49 59
> e: dorthe.arndt@ugent.be
> URL:  http://multimedialab.elis.ugent.be
> 
> 
> 
>