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

Dan Connolly wrote:
> On Sat, 2006-06-10 at 20:32 +0200, jos.deroo@agfa.com wrote:
> [...]
> > > 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)
>
> Ah... good... that was quick! I thought the r:source
> issue was going to be hard.

It was hot weather here, and that helps :)
The changes were

http://eulersharp.cvs.sourceforge.net/eulersharp/2006/02swap/euler.yap?r1=1.54&r2=1.57
http://eulersharp.cvs.sourceforge.net/eulersharp/2004/01swap/src/euler/EulerRunner.java?r1=1.74&r2=1.75
http://eulersharp.cvs.sourceforge.net/eulersharp/2004/01swap/src/euler/Euler.java?r1=1.142&r2=1.143


> >  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

> Yes, quite!
>
> Hmm... as you said earlier, the Inference steps in those
> proofs don't explicitly give bindings. I wonder why check.py
> thinks that's OK. I'll have to look into whether that's
> a feature or a bug.

That would be good to know. What I also see is that
the output of otter and prover9 is without bindings
e.g. http://www.agfa.com/w3c/euler/graph.out.n3
given http://www.agfa.com/w3c/euler/graph.in.n3
and similarly for E theorem prover
http://www.agfa.com/w3c/euler/graph-proof.tstp
given http://www.agfa.com/w3c/euler/graph.tstp

I could make another attempt to explicitly give
bindings (having an idea via adding instrumentation
premise to the rules but must be careful to keep
the speed of the engine reasonable...)
 
> I see lots of stuff that needs more testing...

Right, that's what I also see in our stuff...

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

Received on Sunday, 11 June 2006 11:32:08 UTC