W3C home > Mailing lists > Public > public-owl-comments@w3.org > September 2011

Scope of haskey?

From: Alan Ruttenberg <alanruttenberg@gmail.com>
Date: Wed, 14 Sep 2011 21:56:04 -0400
Message-ID: <CAFKQJ8mN5r1-Pf+mKXBQqw33hqknQx7rL=P99S_NikACc9xcSA@mail.gmail.com>
To: 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>, Bill Duncan <wdduncan@gmail.com>
Is the following ontology consistent or not?


SubClassOf(ex:c DataHasValue(ex:p "1"))
HasKey(owl:Thing () (ex:p))
ClassAssertion(ObjectComplementOf(ex:c) _:foo)
DataPropertyAssertion(ex:p _:foo "1")
ClassAssertion(ex:c ex:o)

The relevant bit of the specs seem to be in the structural specification


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

And in the direct semantics:


a denotes an individual (named or anonymous);


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

HasKey( CE ( OPE1 ... OPEm ) ( DPE1 ... DPEn ) )	
∀ 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.

Received on Thursday, 15 September 2011 01:57:11 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:01:30 UTC