Re: log:definitiveDocument

Tim,

> You do keep up to date!  I hadn't finished writing it up.
> But you see cvs changes of course.

It's a very clear write up, and cvs is very helpful!
(we still lag a lot behind cwm crypto which seems
so crucial in all repects, certainly in healthcare)

>   I tried Euler. I wasn't sure how to get the bindings from it.

I see, they're not in the proof evidence
it's a big missing piece which we didn't
realize 2 years or so ago when we made
a primitive form of SOUND ARGUMENT
(as nested ground implications which
are longhand for true => true)
but I hope to improve on that, at least
while seeing your reason.n3

> Or does it just check consistency?

Well, it's just finding some proofs
for entailment testcases and in some
cases proofs for inconsistencies or
incompletenesses, but it's certainly
not complete while standing alone;
maybe Socratic completeness, using
a set of interoperating engines
could work out...

>  I should go back and find your
> medical
> x-ray example.  I just haven't put in the time I should have.

It's actually on the web at
http://www.agfa.com/w3c/2002/10/medicad/op/
and cwm and euler usage is just

cwm http://www.agfa.com/w3c/2002/10/medicad/op/lldmD.n3
http://www.agfa.com/w3c/2002/10/medicad/op/lldmP.n3 --think

java Euler http://www.agfa.com/w3c/2002/10/medicad/op/lldmD
http://www.agfa.com/w3c/2002/10/medicad/op/lldmP
http://www.agfa.com/w3c/2002/10/medicad/op/lldmC

and is giving consistent evidence everywhere
just that datatyping of e.g. the measurement data
is not yet precise and we have missing OWL pieces
but it's used to testcase that tree like math formulas
can be avoided, just have plain RDF graphs which
are of course ideal for merging with related stuff
and even the performance is in a sense much better
than we had before with our clumsy implementation
with functional term as bnode trees and I think
that improvement comes from the engine that can
just look to what is needs to realize it's goals.

> Yes. you have got it.
>
> I think the axiom is in fact (distinguishing between documents and
> formulae)

oops, forgot that again...

> {?p log:definitiveDocument ?d. ?d log:semantics ?d. log:includes {?s :p
> ?o}} <=> {?s :p ?o}.

right, so
?d log:semantics ?f. ?f log:includes {?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!).

OK, that's right and we don't have disproves either
and also sometimes a lot of steps for iff's ;-)


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

Received on Thursday, 6 February 2003 19:06:54 UTC