Re: same-syntax extensions to RDF

[I've cut out lots of stuff that is not immediately relevant to the two
points I'm trying to make here.]

From: Sandro Hawke <sandro@w3.org>
Subject: Re: same-syntax extensions to RDF 
Date: Thu, 16 Dec 2004 00:11:38 -0500

[...]

> > No surprise, but that is only because there is nothing here to criticize.
> > 
> > What counts as a formula?  What counts as a variable? (Any RDF name??)  

[...]

> > You need to at least give a sketch of the comprehension principles.  (There
> > are lots of examples in the OWL S&AS document.)
> 
> I'm unclear how the comprehension principles are different from the
> axiomatization of the system.   Let me skip this one for now.

This is a vital part of the exercise.  

In your formalization does
	a r b .
	c r d .
entail the encoding of the conjunction of a r b . and c r d . ?

No.  It doesn't, in part because the two triples do not entail that the
triples needed to encode the conjunction are true, regardless of whether
the conjunction itself is true.

The OWL S&AS document has quite a number of just comprehension principles.
Here, you are going to need some principle that says, roughly, whenever two
domain elements encode formula then there is a domain element that encodes
their conjunction.  

[...]

> > I don't think that this works at all.
> > 
> > One thing that you *need* to come out of this is that the theorems of FOL
> > are true in all interpretations (roughly, see below).  So, for example, you
> > need to have the encoding of
> > 	Axy Pxy v ~Pxy
> > be true in all interpretations.  How are you going to get this to do
> > through?
> 
> So, I don't know the best way to explain this.   I convinced myself it
> would work by writing FOL axioms and letting Otter prove results.  For
> example, I would write
> 
>    -(all x y (p(x,y) | -p(x,y)))
> 
> (that is, the negation of your above formula), run my
> otter-to-LX-triples code to turn it into a reified formula
> like
>     rdf(s1, rdf_type, lx_Sentence).
>     rdf(s1, lx_negated, s2).
>     ....
> 
> then mix in a few pages of axioms explaining what lx_negated, etc, all
> mean in such a context.

> Then I'd let Otter run until it found a contradiction, proving your
> original formula was entailed by my axioms.

So?  What does this show?  In particular, where did the axioms come from?
For this to prove anything you have first show that the axioms come from
your semantic theory.  The only stuff that you so far are entitled to
axiomatize is http://www.w3.org/2002/08/LX/RDF/v2.n3.  Where in this is
there something that entitles you to say that a conjunction is true if both
its conjuncts are true?

Second, you haven't shown that just because the encoding of the negation of
a formula has no models that the encoding of the formula is true in all
interpretations.  Remember, you have to show that you are ending up with
FOL.  You can't use theorems from FOL (or propositional logic, or whatever)
until then.  For example, you might have done something that makes all
encodings have no models.

[...]

> Is this making any more sense now? 

Not yet.

Your first task should be to demonstrate that the encoding of a conjunction
follows from the encoding of its conjuncts.  The only tools that you get to
use are the RDF(S) model theory, an RDF(S) document that provides
information about your encoding vocabulary, and any extra semantic
conditions that you write down.

Section 4 of RDF Semantics shows how RDFS is specified as an extension to
RDF in the form of a set of semantic conditions and a set of RDF triples.
This is a very simple semantic extension.  

A more complex extension is given in Section 5 of OWL S&AS.  Any extension
to FOL is going to be more at this level of complexity than the level of
the RDFS extension.

>      -- sandro

peter

Received on Thursday, 16 December 2004 10:11:47 UTC