Re: DTTF: my summary from Jeremy Carroll on 2002-04-25 (www-webont-wg@w3.org from April 2002)

From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
Date: Thu, 25 Apr 2002 14:24:18 +0100
To: <www-webont-wg@w3.org>
Message-ID: <JAEBJCLMIFLKLOJGMELDKENHCDAA.jjc@hplb.hpl.hp.com>

> I need to justify (at least a little) the yes under circular test case
for
> the axioamtic with explicit comprehension approach.

Premise
John child John .

Conclusion
John rdf:type _:1 .
_:1 rdf:type daml:Restriction .
_:1 rdf:onProperty child .
_:1 rdf:hasClass :_1 .


Intermediate step A.

John rdf:type _:2 .

_:1 rdf:type daml:Restriction .
_:1 rdf:onProperty child .
_:1 rdf:hasClass _:one .
_:one rdf:type daml:Class .
_:one daml:oneOf _:list .
_:list rdf:type daml:List .
_:list daml:first John .
_:list daml:rest daml:nil .

(This follows from two explicit comprehension axioms).

Intermediate step B.

John rdf:type _:one .

Then the conclusion follows by deleting triples.

Jeremy

Received on Thursday, 25 April 2002 09:24:48 UTC