Re: same-syntax extensions to RDF

> In general this is much to vague.  You don't need to (at this stage) dot
> all the i's and cross all the t's, but this is much more like waving a
> magic wand.  Specific comments are embedded below.

Sorry, I thought this kind of sketch would be easiest for both of us.
I honestly don't know which details are useful to you and which are
tedious.

> >           _:x rdf:type lx:Sentence.                   # implied
> Why implied?
> >           _:x rdf:type lx:UniversalQuantification.    # implied
> Why implied?
> >           _:x lx:univar _:y.
> >           _:y rdf:type lx:UniVar.                     # implied
> Why implied?
> >           _:x lx:negated _:z.
> >           _:z rdf:type lx:Sentence.                   # implied
> Why implied?
> >           _:z rdf:type lx:Triple.                     # implied
> Why implied?

All the implied triples are implied by the LX OWL ontology.  The domain of
lx:univar is lx:UniversalQuantification, a subclass of lx:Sentence.

I was lazy, though, and the URL I gave doesn't dereference properly.
The last LX ontology published included FalseSentence, so it doesn't
actually handle the Liar at all.  It's at 

   http://www.w3.org/2002/08/LX/RDF/v2.n3

I'll happily clean that stuff up if it'll help.

> >           _:z lx:subjectTerm _:y.
> >           _:z lx:predicateTerm _:rdftypeTerm.
> >           _:z lx:objectTerm _:rdfResourceTerm.
> >           _:rdftypeTerm rdf:type lx:Constant.    
> >           _:rdfResourceTerm rdf:type lx:Constant. 
> > 
> > 
> >     I don't think there are any surprises here.  I'm just saying that
> >     a universal quantification exists of some triple; the universally
> >     quantified variable is the subject of the triple, and the predicate
> >     and object are constants.   I have neither asserted this sentence
> >     nor connected those constants with rdf:type and rdf:Resource yet.
> 
> 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??)  

The excercise here is to describe the syntactic structure of vanilla
FOL.  There are classes: Sentence, Formula, QuantifiedFormula,
Conjunction (or ConjunctiveFormula or some such), ConstantSymbol (or
Constant or Symbol or something, VariableSymbol (or Variables), etc.
These are all classes.  The individuals in these classes are
particular symbols or sentences or whatever.  There is no connection
between the meaning of these and the RDF/OWL semantics -- OWL just
lets us find certain kinds of syntax errors and take certain kinds of
syntactic shortcuts (leaving out the "implied" triples).

So most of the LX ontology is just a straightforward transcription of
a textbook description of FOL syntax into the slightly odd world of
RDF triples, where rather than the BNF

    <conjunction> ::= <formula> '&' <formula>

we have Conjunction as a class, and two properties conjLeft and
conjRight with domain Formula and range Conjunction.  When I was first
playing with this idea, I wrote a program to parse Otter's FOL syntax
and produce triples, and another to match these patterns of triples
and reproduce the original Otter formulas.  (I called this syntactic
loopback testing.)

Drew McDermott and Dejing Dou wrote about DRS doing basically the same
thing, although I don't think they were as careful about it.

So what counts as variable?  The class lx:Variable has two disjoint
subclasses lx:UniVar and lx:ExiVar (a distinction not usually made in
FOL syntaxes, but which I found useful).  Instances of those classes
are variables.  _:y is declared to be one such instance.  Not the
bnode, of course -- the thing denoted by the bnode _:y.

> 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.

> > 2.  Connection
> > 
> >     I see two approaches to connecting those constant symbols
> >     (_:rdftypeTerm and _:rdfResourceTerm) to RDF.  The one that I've
> >     had the most success implementing looks like this:
> > 
> > 	  _:rdftypeTerm lx:denotation rdf:type.
> >        	  _:rdftypeTerm lx:denotation rdf:Resource.
> > 
> >     This says that reified terms map to the given individuals in all
> >     models.  It's trivial to axiomatize.
> > 
> >     Another approach (which TimBL's reification vocabulary uses) would
> >     use triples like this:
> > 
> > 	  _:rdftypeTerm lx:text 
> >                       "http://www.w3.org/1999/02/22-rdf-syntax-ns#type".
> >           _:rdfResourceTerm rdf:type lx:Constant.
> >                       "http://www.w3.org/1999/02/22-rdf-syntax-ns#Resource"
> .
> > 
> >     which is appealing in keeping RDF and the described logic
> >     separate, but then they need some extra-logically machinery to be
> >     re-combined.   
> 
> I'm not sure why you need this at all.  Why not just do it directly, i.e.,
> have 
> 	_:z lx:objectTerm rdf:Resource.
> above?

Because the range of lx:objectTerm is a term in the reified FOL, an
lx:Variable or lx:Constant or maybe some kind of function term.
Without that separation, variables *would* be hopelessly mixed in.

> > 2.  Assertions 
> > 
> >     So how do we assert this sentence, _:x ?
> > 
> >     The obvious approach is to say 
> > 
> >           _:x rdf:type log:Truth
> > 
> >     which might work for cwm/n3's reification which lacks negation
> >     (it's roughly positive Horn), but for FOL (which I'm proposing
> >     here) it becomes trivial to construct a Liar paradox.  So that's
> >     no good.
> > 
> >     The alternative I propose is to say, instead:
> > 
> >          _:x rdf:type lx:Usable
> > 
> >     The definition of Usable is merely this: for a sentence to be
> >     lx:Usable, it must be true.  There may be true sentences which are
> >     not lx:Usable.  Nothing follows from knowing that a sentence is
> >     not lx:Usable.
> > 
> >     The sentence S1 which says "S1 is not Usable" is true.  (If S1 were
> >     false, S1 would be Usable, which would mean (since Usable implies
> >     true) S1 would be true, which contradicts the premise.  If S1 were
> >     true, ... no problem.)   
> > 
> >     The sentence S2 which says "S2 is Usable" isn't a problem either.
> >     If it's true, then S2 is Usable, which is consistent with S2 being
> >     true.  If it's false, then it's not Usable, which is also
> >     consistent with S2 being False.
> > 
> >     My intuition here is that some class of sentences is
> >     "problematic", and we don't want to talk about whether those
> >     sentences are true or false.  So Usable is basically: true and not
> >     problematic.  But by not separating those in the language not
> >     naming True, False, and Problematic in the language, we keep the
> >     language itself (and the reasoners) clear of the problematic zone.
> 
> 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.

More generally, I had a test suite of formulas, each of which I would
encode as triples and then let otter prove from my axioms and the
triples.   I called this semantic loopback testing.

I did several versions of these axioms, playing with various designs.
Two of them are 
    http://www.w3.org/2002/08/LX/RDF/ax3.20020822T1630
    http://www.w3.org/2002/08/LX/RDF/ax4.20020822T1630
which I talked about in
    http://www.w3.org/2002/08/LX/RDF/layering.html
aka http://lists.w3.org/Archives/Public/www-rdf-logic/2002Aug/0093

There may well be flaws in those axioms; I haven't looked at them
since then, except briefly tonight, because more pressing issues took
over.  I think those particular axioms have a less clear notion of
lx:Usable and are still subject to problems involving self-reference.

Is this making any more sense now? 

     -- sandro

Received on Thursday, 16 December 2004 05:08:40 UTC