Re: Summary and some analysis: New Semantics Initiative

>On Wed, 2002-06-12 at 16:01, R.V.Guha wrote:
>[...]
>
>>  I would like to get a wider sample, especially from the folks building
>>  stuff (like Libby, Connolly, ...).
>
>I prefer an axiomatic approach inasmuch as it allows me to use
>the machine to check my work etc.
>
>I'm stil mulling over details of this approach; in particular,
>stuff like
>
>"Axiom schemes do not take the language beyond first-order, since all
>the instances are first-order sentences and the language is compact, so
>if any Lbase sentence follows from (the infinite set of instances of) an
>axiom scheme, then it must in fact be entailed by some finite set of
>instances of that scheme. "
>  -- http://tap.stanford.edu/SemanticWebSemantics.html
>
>give me pause,

Well, maybe we will just punt on axiom schemes. There is no need for 
Lbase to have a BNF for axiom schemes. But the point about finiteness 
and compactness is standard logic textbook stuff, honestly.

>as does:
>
>"Since relations are first-class entities in Lbase, we can express this
>relationship with an axiom:
>
>(forall (?x ?y) (rdf:type(?x, ?y) <=> ?y(?x))) "

Right, you *should* pause there. By all means object to/ comment on 
particular axioms. This one in particular could be argued over (and 
could in fact be omitted altogether if y'all really don't like it; I 
don't think Guha likes it much either :-.)

Part of the whole Lbase idea is to enable this kind of discussion to 
be done more easily and without fear of wrecking the whole thing (as 
changes to an MT are liable to do.) I.e., Im saying, join in.

BTW, heres a proposed change to the above;

(forall (?x ?y)(rdfs:Class(?y) => (rdf:type(?x,?y) <=> ?y(?x) ) ) )

In other words, *for rdfs classes*, having that class as type can be 
seen as predicating the category. That is weaker (and more accurate) 
than saying that ALL property predications are equivalent to rdf:type 
assertions.

If you prefer, we could put this axiom and the resulting 
predicate-style versions of the closure rule implications into an 
appendix.

>	-- http://www.coginst.uwf.edu/%7Ephayes/RDF%28S%29_based_on_Lbase.html
>
>I agree with Graham that...
>"- in the description of axiom schemata, it is not clear how one is
>expected to distinguish "schematic variables" from non-substitutable
>values."
>
>I'm quite happy with the "menzel indrection trick" in the present model
>theory. I'm still noodling on the corresponding bits of the Lbase stuff.

Its exactly the same trick, but it has to be said differently because 
the syntax is more general; we have to allow any arity in the 
relations. (If we allow similar freedom in functions it gets much 
more complicated, which is why we decided to stick to fixed-arity 
function symbols. I think this will be enough for any conceivable SW 
use, particularly as strictly speaking we don't need functions at 
all, since we have equality.)

>Another technical reservation I have is committing to classical
>negation. Based on discussion with TimBL and study of
>systems like Isabelle, I don't think the law of the excluded
>middle is a good thing to commit to for the semantic web.

Ah, that is a deeper issue. Still, Isabelle contains all of classical 
logic as well as intuitionist. (But the basic point is that systems 
like Isabelle are intended for use with program specification and 
verification, not simple ontologies. I doubt that the SW is going to 
be centrally concerned with describing recursion.)

>   http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
>
>I have to admit that I can't think of a way to make these issues
>show up in RDF 1.0 nor RDFS. But the premise of this approach
>is that the same base logic works for higher layers too.

Well, for the layers that we can currently forsee, which is basically 
DAML/OIL/OWL ish kinds of things, and maybe up to something like 
KIF/CL. If one wants to get into the headier areas inhabited by 
HOL-ML or LCF, then one would need to use a more powerful Lbase; but 
that's OK, as long as we can map this one into that (which we almost 
certainly would be able to do.)

>Maybe I'll noodle on some test cases that involve webont-ish
>vocabulary...

By next week I should have a draft of DAML-in-Lbase for you to noodle 
some more.

Pat

-- 
---------------------------------------------------------------------
IHMC					(850)322 0319   cell
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax

Received on Friday, 14 June 2002 12:20:37 UTC