Re: Scope of haskey?

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 Diret Semantics.

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:52 UTC