Re: semantic web proof, curry/howard isomorphism, N3/turtle syntax and semantics stuff

Harry,

> Jos,
> 
> jos.deroo@agfa.com wrote
> > and while that thesis does seem to cover lots of useful
> > ground, I don't see the curry/howard stuff there.
> > 
> >
> > That is true; that was a challenge that was left :-)
> > 
>     My intuition tells me that some sort of small functional core that 
used
> RDF as a sort of typing system might be they way to go for Web Services
> as a lightweight alternative to BPELWS. It's unclear to me if you can
> squeeze N3-Proofs into some Curry-Howard isomorphism, but if there is a
> formal proof theory and proofs can be simplified, it should in theory be
> possible. Proving it is an entire another matter :) and first of course
> N3 rules would need to be given a  proof theory to underlie and maybe
> clarify the work it obviously already does in practice.

A similar neutral ground I think could be found with pi-calculus
in the sense that it can bridge the "declared knowledge" to
"execution environment" gap and we are testcasing that
and it again all turns around N3 based proofs.

> > ) the
> > "Turning proofs into running code" is now more turned into
> > generating proofs of the form
> >
> > [ a r:Proof;
> >   ... # justification components expressed in reason.n3
> >   r:gives {
> >     ... # a theory expressed as a bunch of N3 rules
> > }].
> >
> > using rule induction i.e.
> >
> > Given
> >   Background Knowledge BK
> >   positive Examples E+
> >   negative Examples E-
> > such that
> >   BK does not entail E+
> >   BK does not entail E-
> >
> > then with induction we can find
> >   Hypothesis H
> > such that
> >   BK and H entails E+
> >   BK and H does not entail E-
> >
> > where
> >   BK is a set of theories that are not necessarily asserted
> >   E is any extension set (even the extension of log:implies rules
> >     in which case the E- are headless rules ie integrity constraints)
> > The justification of that H (using reason.n3 ontology) is a closure
> > (in the sense that such proof evidence can be reused in further
> > abduction plus justification).
> > 
>     Quite cool. If you have any URIs that link to code at some point,
> throw them my direction!

Stay tuned; "the future is longer than the past" :-)
At this moment we focus around an implementation like

                  REST
                   /\
                   || N3
                   \/
             ,------------,
             |    Codd    |
             |     /\     |
             |     || Yap |
             |     \/     |
             | ,--------, |
             | | Euler5 | |
             | '--------' |
             '------------'

http://eulersharp.sourceforge.net/2006/02swap/
and a whole bunch of test cases.


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

Received on Thursday, 7 September 2006 23:56:41 UTC