Anonymous Individuals

From OWL
Revision as of 15:07, 19 May 2008 by BijanParsia (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

In OWL 1.0 Anonymous individuals are allowed and are rendered as RDF bnodes (see, e.g. http://www.w3.org/TR/owl-ref/#Individual), subject the constraint that these anonymous individuals can only be related in tree-shaped ways.

Issue 3 notes that this feature seems to be missing from the OWL 1.1 submission.

Boris Motik Raises the issue of whether we treat anonymous individuals as Skolem constants instead

Issue 23 (which has been rejected) asks whether such individuals could be given names, so that two anonymous individuals could be declared different. (pfps 09:06, 14 January 2008 (EST) Giving names to "anonymous" individuals would also give rise to undecidability, by equating them and thus turning tree-shaped structures into effectively arbitrary graph-shaped structures.)

Issue 46 asks for relaxing the restriction on the tree-shaped relatedness, but Boris Motik notes that allowing this would make the language undecidable.

The table below satisfies Action 132.

Entailments for given semantics
Snippet qua variable qua local names Comment
s p _:o s p _:o s p _:o Single triples entail themselves.
s p _:o s p _:o1. s p _:o1. BNodes should be renamable. This requires some trickery for bnodes as names.
s p _:o _:s p _:o1.
_:s p _:o2...
s p _:o1. Under variable semantics we can arbitrarily inflate a graph with new BNodes. Under name semantics we definitely don't want to have multiple new names, but there is a question of whether to preserve going from a URI/Literal to a BNodes should be preserved.
s p _:o1.
s p _:o2.
s p _:o. s p _:o3.
s p _:o2.
Under variable semantics, leaning is a form of entailment. Under name semantics, it is a separate operation.
s p _:o ClassAssertion( s SomeValuesFrom( p owl:Thing ) ) ClassAssertion( s SomeValuesFrom( p owl:Thing ) ) Replace _:o with o and the entailment holds anyway. This corresponds to the general proof rule, Existential Generalization.
ClassAssertion( s SomeValuesFrom( p owl:Thing ) ) s p _:o This shows that BNodes are *not* syntactic sugar for existential variables on the name reading. This is a key entailment to *block*, IMHO.