W3C home > Mailing lists > Public > public-owl-wg@w3.org > February 2008

RE: the other DAML+OIL semantics

From: Michael Schneider <schneid@fzi.de>
Date: Fri, 8 Feb 2008 00:24:23 +0100
Message-ID: <0EF30CAA69519C4CB91D01481AEA06A06C315D@judith.fzi.de>
To: <public-owl-wg@w3.org>
Cc: <dlm@ksl.stanford.edu>, <fikes@ksl.stanford.edu>, "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
[Sent to OWL-WG and to the authors of the DAML+OIL axiomatic semantics


I claim that the axiomatic semantics for DAML+OIL, given by


is inconsistent.

(1) Peter Patel-Schneider observes (see bottom of this mail) that

    rdf:Resource = rdfs:Class

(2) The class rdf:Property is non-empty, because of the axiom


    (Type type Property)

(3) The class rdfs:Class is non-empty, which follows from (1) and (2).

(4) The classes rdf:Property and rdfs:Class are disjoint, because of the


    (not (and (Type ?x Property) (Type ?x rdfs:Class)))

>From (1), (2), (3) and (4) follows the claimed inconsistency.

Best regards,
Michael Schneider

Peter F. Patel-Schneider wrote on Thursday, February 07:

>owl:Thing = rdfs:Class = rdf:Resource = rdf:Property  


>PS: The above can be inferred as follows from axioms and theorems in 
>- the other versions of the document appear similar.
>(<=> (FunctionalProperty ?fp)
>     (and (Type ?fp Property)
>          (forall (?s ?v1 ?v2)
>                  (=> (and (PropertyValue ?fp ?s ?v1)
>                           (PropertyValue ?fp ?s ?v2))
>                      (= ?v1 ?v2))))) [FunctionalProperty axiom 1]
>(FunctionalProperty range) [range axiom 2]
>(<=> (PropertyValue range ?p ?r)
>     (and (Type ?p Property)
>          (Type ?r rdfs:Class)
>          (forall (?x ?y) (=> (PropertyValue ?p ?x ?y)
>                              (Type ?y ?r))))) [range axiom 3]
>(PropertyValue range subClassOf rdfs:Class)     [range theorem 1]
>(PropertyValue range range rdfs:Class)     	[range theorem 2]
>(PropertyValue range type rdfs:Class)     	[range theorem 3]
>(PropertyValue range subject Resource)     	[range theorem 4]
>(PropertyValue range predicate Property)     	[range theorem 5]
>(PropertyValue range object Resource)     	[range theorem 6]
>(PropertyValue range subPropertyOf Property)    [range theorem 7]
>(<=> (PropertyValue subClassOf ?csub ?csuper)
>     (and (Type ?csub rdfs:Class)
>          (Type ?csuper rdfs:Class)
>          (forall (?x) (=> (Type ?x ?csub)
>                           (Type ?x ?csuper))))) [subClassOf axiom 2]
>(PropertyValue subClassOf Class rdfs:Class) [class axiom 1]
>(Type Thing Class) [Thing axiom 1]
>(Type ?x Thing) [Thing axiom 2]
>From [Thing axiom 2] and [range axiom 3] with the assistance of 
>[Thing axiom 1], [class axiom 1], and [subClassOf axiom 2] we get
>(<=> (Type ?p Property)
>     (PropertyValue range ?p Thing))
>From [FunctionalProperty axiom 1] and [range axiom 2] (and range
>being a property - exercise for the reader) we get
>(forall (?s ?v1 ?v2)
>   (=> (and (PropertyValue range ?s ?v1)
>            (PropertyValue range ?s ?v2))
>       (= ?v1 ?v2)))
>Then from the range theorems (and the various properties being
>properties - exercise for the reader) we get the result.

Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555

FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

Received on Thursday, 7 February 2008 23:24:35 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:42:02 UTC