Re: DTTF: my summary

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> · This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:49 GMT

> 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