Re: log:definitiveDocument

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