Re: Scope of haskey?

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 Thursday, 15 September 2011 16:06:58 UTC