Axiomatic Semantics of OWL

A validated set of first-order axioms for OWL, with discussion, is 
available at
http://www.kestrel.edu/home/projects/DAML/owl/axiomatic.html
   or
http://www.ai.sri.com/daml/owl/axiomatic.htm

Comments are solicited.

Here is the abstract for the discussion:

Abstract:

The constructs of the Web Ontology Language (OWL) have been described in 
a first-order axiomatic theory 
<http://www.kestrel.edu/home/projects/DAML/owl/axioms.sw>.   A theorem 
prover was used to ensure that intended consequences follow from the 
axioms.  The theorem prover searched for, and failed to find, 
inconsistencies in the axioms.  Several new consequences of the axioms 
were discovered by the theorem prover, redundant axioms were eliminated, 
and other axioms were simplified.  The axiomatic theory of OWL, with a 
first-order theorem prover, may be used as a reasoner for the Full 
version of OWL.