Re: log:definitiveDocument

Tim,

W.r.t. those bindings, we have done something like
  explain the substitutions in the proof as
    {... ?s = :a. ?p = :b. ?o = :c. ?s ?p ?o} log:implies {:a :b :c}.
It actually seems as if one can do everything with log:implies (and
conjunction)
or at least a lot...
There are some examples in http://www.agfa.com/w3c/euler/etc5-proof.n3

-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/


                                                                                                                   
                    Tim                                                                                            
                    Berners-Lee          To:     Jos De_Roo/AMDUS/MOR/Agfa-NV/BE/BAYER@AGFA                        
                    <timbl@w3.org>       cc:     www-archive@w3.org                                                
                                         Subject:     Re: log:definitiveDocument                                   
                    2003-02-06                                                                                     
                    11:44 PM                                                                                       
                                                                                                                   
                                                                                                                   




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 Sunday, 16 February 2003 17:47:34 UTC