- From: Tim Berners-Lee <timbl@w3.org>
- Date: Thu, 6 Feb 2003 14:44:34 -0800
- To: "Jos De_Roo" <jos.deroo@agfa.com>
- Cc: www-archive@w3.org
Jos,
You do keep up to date! I hadn't finished writing it up.
But you see cvs changes of course.
I tried Euler. I wasn't sure how to get the bindings from it.
Or does it just check consistency? I should go back and find your
medical
x-ray example. I just haven't put in the time I should have.
Yes. you have got it.
I think the axiom is in fact (distinguishing between documents and
formulae)
{?p log:definitiveDocument ?d. ?d log:semantics ?d. log:includes {?s :p
?o}} <=> {?s :p ?o}.
In principle is a implication both ways (iff) you can also disprove s
p o by showing that the document does not
include it. cwm doesn't do that, because it doesn't prove things
false. (yet - anyway!).
Tim
On Tuesday, Feb 4, 2003, at 19:09 US/Eastern, Jos De_Roo wrote:
> Tim, sorry to come in again just before the TAG f2f meeting,
> but I was wondering about implementing log:definitiveDocument
> and log:definitiveService (they seem like very interesting).
> I think that we would, when loading a fact
> :p log:definitiveDocument :d.
> prepare with a rule
> {:p log:definitiveDocument :d. :d log:includes {?s :p ?o}} => {?s :p
> ?o}.
> but we would (while proving)
> 1/ make sure that ?s and ?o are bound
> 2/ not look to other :p facts or rules
>
> Is that what is intended with log:definitiveDocument ?
>
> -- ,
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 6 February 2003 17:44:07 UTC