Re: use of log:semantics

----- Original Message -----
From: <jos.deroo.jd@belgium.agfa.com>
To: <timbl@w3.org>
Cc: <w3c-rdfcore-wg@w3.org>
Sent: Thursday, October 18, 2001 9:51 PM
Subject: Re: use of log:semantics


>
> Tim,
>
> > I was going to ask you about whether your were thinking of building
> > in functions to Euler.
>
> Yes, and I was thinking the last couple of weeks to ask you
> about which ones and this is the nicest work I can imagine!
>
> > The functional Properties I am using for this sort of stuff at the
moment
> > are:
> >
> > log:semantics    - The graph (formula) you get if you get a
representatioon
> > of somthing and parse its semantics
>
> ok, seems a must
>
> > log:conjunction - The graph you get from merging a list of graphs
> > log:conclusion  -  The graph you get from taking all the rules in a
graph
> > and applying them
> >                           the graph, putting new statements into the
graph.
> > Closure under forward chain inference.
> >                           Same as cwm -think
>
> log:conclusion will be a challenge
> we've done attempts with a query _:s _:p _:o .

I would suggest then you don't use it - define a log:entails  (say) which is
the equivalent of
the combination   of  conclusion and includes.   Because in this case, it is
what the test case needs, after all, and what Euler will naturally test.

I think maybe we will need mixtures of forward and backward reasoning.  When
dealing
with small datasets, cwm can always replace   F log:entails :G with
F log:conclusion [ log:includes :G ]  --- it just doesn't scale well!

> > log:includes     -  A binary operator, true if one graph is a subgraph
of
> > the other, modulo a bit of inference and
> >                          variable subsitution.
> > log:directlyIncludes     -  A binary operator, true if one graph is a
> > subgraph of the other, modulo only
> >                          variable subsitution.
>
> we try that along the 'entail' way, and control
> the kind of inferencing with what Pat calls 'namespace entailment'
>
> > I haven't got conjunction and conclusion running yet.
> > http://www.w3.org/2000/10/swap/test/includes/check.n3
> > is an example of using some of these to check that predicates
> > used in a document are indeed defined in the schema.
> >
> > I have not used "entails under RDFS" - I just merge the RDFS axioms and
then
> > use log:conclusion.
> >
> > So, I would write a test something like
> >
> > { this log:forAll :p, :r, :x, :z.
> >   {    :p rdfs:range :r .  :x :p  :z } log:shouldEntail { :z a :r }.
> > } a :test.
> >
> > Then I would define use of shouldEntail with something *like*
(untested!!)
> >
> > { :T a :test.
> >    :T log:includes { :F log:shouldEntail :G}.
> >    <rdfsRules.n3> log:semantics :R.
> >   [  log:conjunction ( :F  :R) ] log:conclusion  [ log:includes :G ]. }
> > log:implies { :T a :success }.
> >
> > plus a few combinations with notIncludes to do negative tests.
>
> haven't thought how to support that one...

notIncludes in cwm has to involve a recursive call back to a new query,
testing the result, and returning it.   It is quite different to includes.
notIncludes is the way you can spoecifically introduce defaults, and specify
definitive documents without relying on falacious closed world assumptions.

> > I expect if one had a  backward chainer, one would use a proof search
> > instead of
> > the conclusion...includes combination:
> >
> >   [  log:conjunction ( :F  :R) ] euler:supportsProofOf G ]. }
log:implies
> > { :T a :success }.
>
> I will start with the log:semantics
> (and also do () lists) and then log:conjunction
> This is of real great help, thanks!

I am really embarassed that I haven't gone to the trouble of setting up
Euler -- I must!

It is interesting and encouraging that we have forward and backward chaining
systems usefully using the same
data and the same rules!

Tim

> Jos
>

Received on Friday, 19 October 2001 14:00:49 UTC