W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > April 2003

Re: Another Comment on Owl Ref {was: Re: Denotation of owl:Class)

From: Dan Connolly <connolly@w3.org>
Date: 27 Apr 2003 22:08:46 -0500
To: Brian McBride <bwm@hplb.hpl.hp.com>
Cc: Jeremy Carroll <jjc@hplb.hpl.hp.com>, w3c-rdfcore-wg@w3.org
Message-Id: <1051499325.2632.69.camel@dirk.dm93.org>

On Sun, 2003-04-27 at 21:58, Dan Connolly wrote:
> On Sun, 2003-04-27 at 07:04, Brian McBride wrote:
> > Oh dear, I was hoping there was good reason for making the 
> > distinction.  Can someone confirm Jeremy's view.
> 
> I can't. I probably should be able to confirm or deny,
> but I can't.
> 
> At first I was under the impression that owl:Thing
> was disjoint from owl:Class and owl:Property, even
> in OWL Full. But somebody told me that wasn't right;
> in order to make the layering stuff work out,
> owl:Thing is the same as rdfs:Resource in OWL Full;
> at that point,

postscript: actually, at that point, I fired up larch and
tried to transcribe S&AS. I got as far as updating
my work on the RDF Core MT...

----------------------------
revision 1.5
date: 2003/01/31 14:51:05;  author: connolly;  state: Exp;  lines: +19
-19
changed Graph sort to really be a set of triples
----------------------------
revision 1.4
date: 2003/01/29 19:00:09;  author: connolly;  state: Exp;  lines: +66
-12
main result of RDF semantics section 2, interpolation lemma, sort checks
----------------------------
revision 1.3
date: 2003/01/29 18:00:18;  author: connolly;  state: Exp;  lines: +43
-42
section 1 of RDF semantics spec done
----------------------------
revision 1.2
date: 2003/01/29 17:17:53;  author: connolly;  state: Exp;  lines: +88
-108
RDFCoreMT sort checks, though I basically started over and it covers
less of the spec


http://www.w3.org/XML/9711theory/RDFCoreMT.lsl


I tried to prove the interpolation lemma with the larch prover,
but it fell over and I (re-)discovered it's not really
maintained any more.
(the larch sort-checker still works; it's written
in C; but the larch prover is written in clu or
something that has gone the way of the dinosaur)

Then I started looking a coq (since it's a
maintained debian package) but I didn't
get that far.

>  I decided I didn't care enough
> to count angels on heads of pins further; all the
> test cases I'm interested in work the way I expect
> them to work, so I'm fat-dumb-and-happy.

Graham's mention of haskell reminds me that I'd
like to survey the landscape of formal-hacking
tools again, I think.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Sunday, 27 April 2003 23:08:27 EDT

This archive was generated by hypermail pre-2.1.9 : Wednesday, 3 September 2003 09:57:02 EDT