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

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?

> > 2. add r:source <http://www.agfa.com/w3c/euler/socrates.n3>
> >    to the 2 parsing steps and take the r:gives off them
> 
> That's a bit more difficult as we currently in the
> euler5 prototype get the input from euler1 which
> does the n3 parsing and the aggregation of input
> fact and rule files and we give the source
> information right now as [ a r:Parsing; r:gives
> (<http://www.agfa.com/w3c/euler/socrates.n3>!log:semantics
> <http://www.agfa.com/w3c/euler/socratesQ.n3>!log:semantics)!log:conjunction

I see... yeah... porting the N3 parser over can be boring work...

I wonder how close we are to generating parsers from n3.n3...
I hope to get back to reconciling my BNF ontology
with timbl's...

 bnf2turtle -- write a turtle version of an EBNF grammar
 http://dig.csail.mit.edu/breadcrumbs/node/85


> It is still a prototype (but runs quite huge test cases)
> and I will look what can change tomorrow :)
> and I will check asap with check.py

Good... I did work on check.py this week, breaking
the great big valid() function into separate
checkConjunction(), checkGMP() etc. routines
and adding some unit tests. I'm doing this to get
my head around the code because I need to do
some work to integrate it with our policy aware
web demo a bit better.

I still don't understand everything it's doing,
but I'm getting there...

http://www.w3.org/2000/10/swap/check.py
v 1.41 2006/06/09 22:16:06

I'm pretty sure Jos knows this, but for others
who may be following along...

It depends on much of the other swap code
(I'm working on reducing that too...).
Our public CVS repository is sync'd every
half hour or something with our development
code...
  http://dev.w3.org/cvsweb/2000/10/swap/

I think you only need the code in that top
level directory (cvs checkout -l) to run
swap, but to test it you need much
of swap/test/* .

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)

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Saturday, 10 June 2006 02:44:08 UTC