RE: the other DAML+OIL semantics

[Sent to OWL-WG and to the authors of the DAML+OIL axiomatic semantics
document.]

Hello!

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

    <http://www.w3.org/TR/daml+oil-axioms>

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

    <http://www.w3.org/TR/daml+oil-axioms#3.2.1>

    (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
axiom

    <http://www.w3.org/TR/daml+oil-axioms#3.1.3>

    (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  

[snip]

>PS: The above can be inferred as follows from axioms and theorems in 
>http://www.ksl.stanford.edu/people/dlm/daml-semantics/daml+oil-
>axioms-october2001.htm
>- 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