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 .

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

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

Jos

Received on Thursday, 18 October 2001 20:51:54 UTC