Inconsistency in DAML+OIL Axiomatic Semantics

The UBOT project has been examining the consistency of the
DAML+OIL axiomatic semantics.  Using an automated theorem
prover, Richard Waldinger found an inconsistency due to
Axiom 8.  This axiom is the following:

Ax8. (<=> (Type ?fp FunctionalProperty) 
          (and (Type ?fp Property)
               (=> (and (PropertyValue ?fp ?s ?v1) 
                        (PropertyValue ?fp ?s ?v2))
                   (= ?v1 ?v2))))

From this axiom one can conclude that every property is
functional.  As there are many properties that are not
functional (such as type), this leads quickly to logical
inconsistencies in the axiomatic semantics.

We suggest that this axiom be changed to:

Ax8. (<=> (Type ?fp FunctionalProperty) 
          (and (Type ?fp Property)
               (forall (?s ?v1 ?v2)
                  (=> (and (PropertyValue ?fp ?s ?v1) 
                           (PropertyValue ?fp ?s ?v2))
                      (= ?v1 ?v2)))))

Ken Baclawski
UBOT Project
College of Computer Science
Northeastern University