Re: Scope of haskey?

Alan,

I added this to the list of errata [1].

Thanks,
Ian

[1] http://www.w3.org/2007/OWL/wiki/Errata


On 15 Sep 2011, at 17:05, Alan Ruttenberg wrote:

> On Thu, Sep 15, 2011 at 3:09 AM, Boris Motik <boris.motik@cs.ox.ac.uk> wrote:
>> Hello,
>> 
>> The ontology should be consistent because keys don't take into account blank nodes. If they did, this might be counterintuitive because keys don't apply to objects introduced by the existentials; hence, this case was excluded by ISNAMED in the Direct Semantics.
> 
> Good. That was my conclusion as well, based on the direct semantics. I
> think, then, that it is worth making this a bit clearer in
> http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/#Keys . Note that
> anonymous individuals are not described as objects introduced by
> existentials in the structural specification. Rather they are
> described as individuals whose names are local to the ontology.
> 
> -Alan
> 
>> 
>> Regards,
>> 
>> Boris
>> 
>> 
>> -----Original Message-----
>> From: Alan Ruttenberg <alanruttenberg@gmail.com>
>> Date: Thu, 15 Sep 2011 02:56:04
>> To: public-owl-comments@w3.org<public-owl-comments@w3.org>
>> Cc: Evren Sirin<evren@clarkparsia.com>; Dmitry Tsarkov<dmitry.tsarkov@gmail.com>; Boris Motik<boris.motik@comlab.ox.ac.uk>; BillDuncan<wdduncan@gmail.com>
>> Subject: Scope of haskey?
>> 
>> Is the following ontology consistent or not?
>> 
>> Prefix(ex:=<http://example.com/>)
>> Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
>> 
>> Ontology(
>> Declaration(Class(ex:c))
>> SubClassOf(ex:c DataHasValue(ex:p "1"))
>> Declaration(DataProperty(ex:p))
>> HasKey(owl:Thing () (ex:p))
>> ClassAssertion(ObjectComplementOf(ex:c) _:foo)
>> DataPropertyAssertion(ex:p _:foo "1")
>> Declaration(NamedIndividual(ex:o))
>> ClassAssertion(ex:c ex:o)
>> )
>> 
>> The relevant bit of the specs seem to be in the structural specification
>> 
>> http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/#Keys
>> 
>> A key axiom of the form HasKey( owl:Thing ( OPE ) () ) is similar to
>> the axiom InverseFunctionalObjectProperty( OPE ), the main differences
>> being that the former axiom is applicable only to individuals that are
>> explicitly named in an ontology, while the latter axiom is also
>> applicable to individuals whose existence is implied by existential
>> quantification.
>> 
>> And in the direct semantics:
>> 
>> http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/#Vocabulary
>> 
>> a denotes an individual (named or anonymous);
>> 
>> http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/#Satisfaction_in_an_Interpretation
>> 
>> ISNAMEDO(x) = true for x ∈ ΔI if and only if (a)I = x for some named
>> individual a occurring in the axiom closure of O
>> 
>> Table 9. Satisfaction of Keys in an Interpretation
>> 
>> Axiom
>> HasKey( CE ( OPE1 ... OPEm ) ( DPE1 ... DPEn ) )
>> Condition
>> ∀ x , y , z1 , ... , zm , w1 , ... , wn :
>>    if x ∈ (CE)C and ISNAMEDO(x) and
>>       y ∈ (CE)C and ISNAMEDO(y) and
>>       ( x , zi ) ∈ (OPEi)OP and ( y , zi ) ∈ (OPEi)OP and
>> ISNAMEDO(zi) for each 1 ≤ i ≤ m and
>>       ( x , wj ) ∈ (DPEj)DP and ( y , wj ) ∈ (DPEj)DP for each 1 ≤ j ≤ n
>>    then x = y
>> 
>> --
>> 
>> The direct semantics is the clearer and I think it says the ontology
>> should be consistent because the haskey axiom is applicable neither to
>> implied individuals that are members of ex:C, nor to the :_foo, and
>> the description of individuals as either named or anonymous.
>> 
>> The structural specification has a slight problem. There the scope is
>> in terms of
>> 
>> "individuals that are explicitly named in an ontology" and
>> "individuals whose existence is implied by existential quantification"
>> 
>> If "individuals that are explicitly named in an ontology" includes
>> both anonymous individuals (which are actually named, in the syntax)
>> and individuals typed namedindividual, then it is at odds with the
>> direct semantics.
>> 
>> If "individuals that are explicitly named in an ontology" only refers
>> to the latter, then the documentation doesn't cover all cases,
>> omitting anonymous individuals.
>> 
>> --
>> 
>> I have tested consistency of the above ontology with Pellet, Hermit,
>> and FaCT++. Pellet says it is inconsistent, Hermit says it is
>> consistent, and FaCT++ gives an exception seemingly to do with
>> incomplete support for key axioms.
>> 
>> I will put up a test case at the test site when it is confirmed what
>> the correct behavior is.
>> 
>> --
>> 
>> I'm not sure it there is a need, but it is worth considering whether
>> some comment on the reasoning problem satisfiability is in order given
>> that it seems that in cases the result of this task depends on in
>> "(CE)C ≠ ∅." whether (CE)C has an element that is named or anonymous,
>> or not.
>> 
>> -Alan
>> 
>

Received on Tuesday, 27 September 2011 18:55:15 UTC