OWL2: 11.2 - Restrictions on the axiom closure

Below are three comments about 11.2 in http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/#The_Restrictions_on_the_Axiom_Closure

1) Define the forest of anonymous individuals.

Michael Schneider raised questions about this a few months ago:
http://lists.w3.org/Archives/Public/public-owl-wg/2009May/0362.html

Based on the description & example, I understand that, given a set of axioms Ax, F is a directed graph with vertices V and edges E such that:

 *   V = the set of all anonymous individuals appearing in the syntactic definition of any of the axioms in Ax.
 *   E = the set of all pairs (_:x, _:y) such that _:y is directly a child of _:x

Please clarify:

 *   what makes an anonymous individual a root of F?
 *   what makes an anonymous individual _:y a child of another anonymous individual _:x?

2) Example on "Restrictions on Datatypes"

Since the restriction involves a strict partial order, I suggest replacing the following:

For example, it can be readily verified that the order < given below fulfills the above conditions.

xsd:string   <   a:SSN   <   a:TIN   <   a:TaxNumber

With this:

For example, it can be readily verified that the partial order <1 given below fulfills the above conditions.

xsd:string   <1 a:SSN  <1   a:TaxNumber
xsd:string   <1   a:TIN   <1   a:TaxNumber

        The total order <2 given below fulfills the above conditions and is also consistent with the partial order <1 given above.

xsd:string   <2   a:SSN   <2   a:TIN   <2   a:TaxNumber

3) Restriction on Simple Roles

The first and second examples would be clearer if you provided the strict partial order instead of a total order and indicated the provenance of the ordering constraints to the axioms.

For the first example, I suggest replacing:

For example, it can be readily verified that the order < given below fulfills the above conditions.

a:hasFather   <   a:hasBrother   <   a:hasUncle   <   a:hasWife   <   a:hasAuntInLaw

With:

For example, it can be readily verified that the partial order <1 given below fulfills the above conditions.

a:hasFather   <1   a:hasUncle   # 1st axiom
a:hasBrother   <1   a:hasUncle   # 1st axiom
a:hasUncle   <1   a:hasAuntInLaw # 2nd axiom
a:hasWife   <1   a:hasAuntInLaw # 2nd axiom

The total order <2 given below fulfills the above conditions and is consistent with the partial order <1 given above.

a:hasFather   <2   a:hasBrother   <2 a:hasUncle   <2   a:hasWife   <2 a:hasAuntInLaw

For the second example, since the axioms are symmetric, it is ambiguous which ordering constraints corresponds to which axiom. I suggest replacing:

To verify this condition formally, note that, for < to satisfy the third subcondition of the third condition, we need a:hasUncle < a:hasBrother and a:hasBrother < a:hasUncle; ...

with:

To verify this condition formally, note that, for < to satisfy the third subcondition of the third condition, we need a:hasUncle < a:hasBrother (2nd axiom) and a:hasBrother < a:hasUncle (1st axiom); ...

- Nicolas.