Re: Encoding RDF graphs and/or n3 formulas in triples (Reification)

----- Original Message -----
From: "Sandro Hawke" <sandro@w3.org>
To: <timbl@w3.org>
Cc: <www-rdf-logic@w3.org>
Sent: Saturday, December 15, 2001 4:55 PM
Subject: Encoding RDF graphs and/or n3 formulas in triples (Reification)


>
> When I was writing my first n3 parser [1], I had it turn each { ... }
> structure (which you then called a Context and now call a Formula)
> into a Set of rdf:Statement objects, using an ontology for sets I made
> up.


For me, context is the relationship between the 4-statement and the formula.
Formula is the class, range of context.

myQuad n3:context :myFormula.


> I no longer think that's quite the right modeling.  Your current logic
> ontology [2] suggests the right thing is to use your log:conjunction
> predicate.  You say its domain is a list of Formulas.  (You call them
> "formulae," but I can't decide whether to say formulee or formuliy so
> I say formuluz.)   If rdf:Statement is a subclass of log:Formula
> (as I think it ought to be), then we can simply say
>     { <a> <b> <c>. }

(I was just taught "formulae", (-ee).  I don't regard it as cannonical as I
don't think my teachers were around when it was pronounced, so I can
imagine there are different schools of thought. I am not fuzzy about plural
or the pronounciation as life is too short and there are two many low
hanging fruit.)

I agree that Statement can be subclas of Formula, the subclass of formulae
with only one statement, ie matching { :p :s :o } for some p,s,o.

> is an rdf:Statement with the usual rdf:subject, etc, information,
> and
>     { <a> <b> <c>.  <d> <e> <f>. }
> is the log:conjunction of a list of the two rdf:Statements given
> there.
>
> Is that what you had in mind?  Does that seem right?

In other words,
{ <a> <b> <c>.  <d> <e> <f>.} log:conjunction ( { <a> <b> <c>.} {<d> <e>
<f>} ).

Yes.

> The one odd thing I see is that log:conjunction doesn't assert its
> resulting formula, unlike log:implies.  For them to match in style, it
> should be either
>     # make a statement of implication, which is an unasserted object
>     [ log:if { ... }
>       log:then { ... } . ]
> or
>     # assert all the statements in a list
>     ( :stmt1, :stmt2 ) a log:trueConjunction.


You are getting at the way cwm processes stuff - that it doesn't
infer from builtins in the ground facts.  I could change what sort of
inference
the machine does.  Doesn't change the meaning, of course.

I chose so far to only implement implies, because it is the building block
with which
one can build so much - you can build the behaviour of other things by
writing axioms
for them in terms of implies.

[[[ For example, the axiom

{  :l string:concatenation :y,  :z} log:implies { :y = :z }.

which would,  on data

("John" "Doe") string:concatenation :myName.

yield under, cwm --think,

"JohnDoe"  = :myName.

and the reverse.  ( i would test it but I'm on the wrong machine ...)

Which is what you would expect.
]]]


> It's kind of a wash which way you go.  "x={...}" lets you turn
> assertions back into an unasserted formula, and "x a log:Truth" lets
> you assert an unasserted formula.  It just might be nice to have all
> the operators-on-formulas behave one way or the other.

Well, at the moment is is sort of mimimal in that it uses log:Truth and
log:implies only,
and anything else you have to bootstrap from log:implies.

I can envisage the  --think=nbtieBgLyfD  options syndrome in which different
sorts fo inference
are turned on and off.  Not evil, but not to be done lightly either.

>  (This might
> help clear up some confusions [in my mind, at least] about log:forAll
> and log:forSome, too.)


Oh, those? They aren't real properties.  They link a symbol and the scope in
which is quantified.  They don't work with the = axiom

{:s :p :o. :p = :q} log:implies  {:s :q :o}.

I  intend to make them a special syntax, and make them invisible to queries.
But for the moment they work (when explicilt excluded from that axiom
{:s :p :o. :x = :y; log:notEqualTo log:forSome, log:forAll} log:implies  {:s
:q :o}.
They are excluded automatically if you have a rule that that you never write
forSome = :x    and you never use the IDs you have used for variabels
foranything else)




>      -- sandro
>
> [1] http://www.w3.org/2001/03/flaten3/
> [2] http://www.w3.org/2000/10/swap/log
>

Tim

Received on Tuesday, 18 December 2001 21:40:15 UTC