Re: Implicit Quantification in N3

Hello,
first of all: Thank you for your answers!
I still have two remaks/questions:


>>
>> 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.
I am a little bit confused here, I thought that sparql handles that case 
different.  If I have the query:

    select distinct ?p ?t where {

     {{{?p a <http://dbpedia.org/ontology/Place>.}}}

     {{{?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }}}

    }




Doesn't it mean the same as:

    select distinct ?p ?t where {

     {?p a <http://dbpedia.org/ontology/Place>.}

     {?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }

    }




So here the quantification seems to be on top level and not just on the 
"mother-graph".


>   
>>     {{?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
>>
>>
>>
>>


-- 
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