W3C home > Mailing lists > Public > www-rdf-logic@w3.org > April 2001

Inconsistency in DAML+OIL Axiomatic Semantics

From: Ken Baclawski <kenb@ccs.neu.edu>
Date: Fri, 13 Apr 2001 20:56:08 -0400 (EDT)
To: www-rdf-logic@w3.org
Message-ID: <Pine.LNX.3.96.1010413180752.21962C-100000@steam>
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
Received on Friday, 13 April 2001 20:56:11 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:38 GMT