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.)
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.|