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>

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
*