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 GMT
This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 July 2008 08:08:50 GMT