Re: reason proof ontology details [was: ... interoperating]

Dan Connolly wrote:
> On Sat, 2006-06-10 at 01:09 +0200, jos.deroo@agfa.com wrote:
> [...]
> > > 1. add a r:Proof on the ultimate step
> > 
> > That was fixed last Sunday and the actual etc5.ref is at
> > http://eulersharp.sourceforge.net/2006/02swap/etc5.ref 
>
> Ah... yes.
>
> Looking over that, I see...
>
>     [ a r:Extraction; r:gives {(1 1) math:sum 2}; r:because [ a 
r:Parsing; r:gives _:kb20]]
>
> But that 1+1=2 formula is actually not the result of parsing a file.
> The reason ontology calls that a r:Fact. Is that an easy
> change to make?

This is now done and also the r:source is fixed
(via quads) and it is so nice to see the check.py for

http://eulersharp.sourceforge.net/2006/02swap/socratesE.n3
http://eulersharp.sourceforge.net/2006/02swap/graphE.n3
http://eulersharp.sourceforge.net/2006/02swap/medE.n3
http://eulersharp.sourceforge.net/2006/02swap/gedcomE.n3
http://eulersharp.sourceforge.net/2006/02swap/exonE.n3

and giving


Wow... and indeed

> This is pretty exciting... we're getting closer
> and closer to filling in the top of the layer
> cake...
>
> "If there is a semantic web machine, then it is a proof validator, not a
> theorem prover."
>   -- http://www.w3.org/DesignIssues/Logic.html
>      (1st appeared in an Apr 2000 draft)

Thanks and have a nice weekend!

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