W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > October 2001

Re: use of log:semantics

From: Tim Berners-Lee <timbl@w3.org>
Date: Thu, 18 Oct 2001 14:42:13 -0400
Message-ID: <019501c15804$9afed530$6801a8c0@CREST>
To: <jos.deroo.jd@belgium.agfa.com>
Cc: <w3c-rdfcore-wg@w3.org>
Jos,

I was going to ask you about whether your were thinking of building
in functions to Euler.

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

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.

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

Tim

----- Original Message -----
From: <jos.deroo.jd@belgium.agfa.com>
To: <timbl@w3.org>
Sent: Thursday, October 18, 2001 7:18 AM
Subject: use of log:semantics


> Tim, there is the "entailment test cases" idea (in the RDFCore WG)
> and the idea is to describe these tests in RDF (actually RDF/NT)
> -- http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2001Sep/0322.html
>
> I just wonder how
>
>   [ tc:graph g1, g2, g3 ] tc:rdfsentail [ tc:graph g4 ].
>
> could be written in more of your log: vocabulary...
> I see there log:semantics, so we could maybe write
>
>   <g1> log:semantics _:lhs .
>   <g2> log:semantics _:lhs .
>   <g3> log:semantics _:lhs .
>   _:lhs mt:rdfs_entail _:rhs .
>   <g4> log:semantics _:rhs .
>
> where mt: is the model theory namespace
> containing #rdf_entail, #rdfs_entail, ...
>
> thoughts?
>
> --
> Jos
>
>
Received on Thursday, 18 October 2001 14:42:16 EDT

This archive was generated by hypermail pre-2.1.9 : Wednesday, 3 September 2003 09:41:06 EDT