- From: Alan Ruttenberg <alanruttenberg@gmail.com>
- Date: Thu, 15 Sep 2011 12:05:59 -0400
- To: Boris Motik <boris.motik@cs.ox.ac.uk>
- Cc: "public-owl-comments@w3.org" <public-owl-comments@w3.org>, Evren Sirin <evren@clarkparsia.com>, Dmitry Tsarkov <dmitry.tsarkov@gmail.com>, Boris Motik <boris.motik@comlab.ox.ac.uk>, BillDuncan <wdduncan@gmail.com>
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