Re: Some thoughts on L-Base

Sando,

  Thank you for your comments. Here are some responses.

1. I completely agree with your request for an actual syntax. Any 
particular theorem prover will have to use a particular syntax and we 
should (eventually) define one. However, we are completely mortified at 
the possibility of this getting mistaken for yet another interchange 
format. Which is in part why the document uses non-ascii things like 
subscripts ... We want to get the message --- that this is a way of 
doing semantics, not exchanging pieces of data --- loud and clear.

2. Access to l-base names (such as urirefs). This too is an 
implementation level issue. I think.

I think we (i.e., SWAD+RDF-IG) should try and build an implementation 
that addresses 1 & 2. That will make it concrete. What do you think?

thanks!

guha


Sandro Hawke wrote:
> I'm writing in response to your L-Base documents [1] [2], which I
> understand are currently in draft form, perhaps on their way to W3C
> Note status.
> 
> I've been working on precisely specifying the semantics of our 
> "log" vocabulary [3], using essentially the same approach, which has
> led me to a few thoughts about your document.
> 
> 1.  Please specify a machine-readable and human-readable syntax
> 
> In [1] you specify a syntax with single letter names and subscripts.
> We get the idea, but that's obviously not practical for machine
> processing (or sending in e-mail!).  In [2] you're using an ascii
> syntax, but it's not the one in [1].  What exactly is the syntax?
> Where is it defined?  (More to the point: where are the
> implementations!?)
> 
> I understand you considered using KIF.  I'm using the formula syntax
> of otter [4].  You could use TPTP's native format [5], although that's
> not very pretty.  Otter's syntax is a lot like what you use in [2],
> except it uses "all" instead of "forall", and symbols like "&" instead
> of "and".  Examples: "all x y exists z (P(x,y,z) | Q(x,z))" and "all x
> (P(x) & Q(x) & R(x) -> S(x))".
> 
> It's plain FOL-with-equality (the way I use it at least), so you do
> need to say rdf(s,p,o) instead of p(s,o), but I consider that a good
> thing; it makes it more clear what's in L-Base and what's in RDF.
> 
> I also use rdf_type instead of rdf:type, which otter would require be
> quoted.   
> 
> Anyway, it doesn't matter what syntax, but I think you do need some
> unambiguously parsable ascii syntax....  You *could* use a layered RDF
> syntax for FOL, like McDermott et al [6] (I have a translator from one
> of them to otter, and plan to write a reverse translator shortly), but
> that would probably just confuse people at this stage.
> 
> 2.  I think it's important to have the text of the urirefs and
> literals available.  I recognize this is not supported by the current
> MT, but I think that's a mistake.  It's information that's available
> to applications and will be used; if we put it out of range of the
> formal semantics, then we leave it unnecessarily to the informal ones.
> 
> My approach is to translate every RDF document to an L-Base WFF using
> only (1) existential variables, (2) the constants zero and
> emptyString, (3) the functions succ(), unicodeCharacter(), strCons(),
> and webDenotation(), and (4) the predicate rdf() as above.
> webDenotation() is the function mapping from strings to the things
> denoted by using those strings as urirefs.  I've left out
> XML-literals, xml:lang, and unicode versioning issues for now.  (There
> are of course, other, equivalent basic sets.  Maybe one that didn't
> touch numbers would be better.)
> 
> I believe this formalization allows RDF layered languages to have
> semantics involving the text of URIRefs, and of literals, while not
> breaking anything.   It does increase complexity (for humans and
> machines), but it's probably worth it.   For my purposes, some
> predicates that Tim B-L uses (eg log:racine) rely on it.
> 
> Note that this formalization does not let you ask about "the"
> identifier for an object, but just about a string which might happen
> to be known to have its webDenotation be the object.   And it
> certainly doesn't grant access to L-Base identifiers or anything.
> 
> In any case, we need some way to convey the information that all RDF
> literals are pairwise not-equal.   If you said how to do that, I missed
> it. 
> 
> ....
> 
> Those are probably my two strong opinions.  I mentioned in earlier
> e-mail that in some cases consistency of axioms may actually be
> provable, eg by finding a model.  
> 
> In general, I'm pretty happy & optimistic about this approach,
> although axiomatizing some common vocabulary terms is very difficult.
> 
> And I haven't a clue what to do with log:contents, which relates a URI
> with the strings you obtain by fetching it.  I guess I'll be able to
> formally define (or at least constrain) it in terms of some
> network-operations ontology.
> 
> Have you guys been thinking about how these semantics might be
> published, and even automatically retreived, from the namespace
> address (or elsewhere)?  
> 
> I guess my real question is this: I see how this stuff is very useful
> for getting logic layering right, but does it come into play at all
> with ontologies for buying books over the web, etc?  I can see it
> fulfilling the same role as DAML+OIL or OWL there, sort of.  Should
> it?
> 
> Or is this really just an on-paper read-by-logicians kind of thing for
> you?
> 
>     -- sandro
> 
> [1] http://tap.stanford.edu/sw/swmt.html
> [2] http://tap.stanford.edu/sw/rdfsem.html
> [3] http://www.w3.org/2000/10/swap/log.n3
> [4] http://www-unix.mcs.anl.gov/AR/otter/
> [5] http://www.cs.miami.edu/~tptp/
> [6] ftp://ftp.cs.yale.edu/pub/mcdermott/papers/McDermottDou02.pdf

Received on Monday, 22 July 2002 12:03:35 UTC