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

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.
> ) 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!

>> I think we actually submitted a paper to TPLP:
>>   http://dig.csail.mit.edu/2006/Papers/TPLP/n3logic-tplp.html
>>   http://dig.csail.mit.edu/2006/Papers/TPLP/n3logic-tplp.pdf
>>     
>
> Thanks for sharing this; it is VERY good and
> N3 remains the best I have seen for years now!
>   
    Yes - N3 is the best. It's already in SPARQL. Hmmm...maybe Dan,
could you clarify what would be needed to get N3 subset Turtle to a Rec.
status so we have  a legit W3C-approved to RDF-XML? I think the RDF
community is already using Turtle quite a bit, and this would further
just make people happy. I can see how Becket. and TimBL are some of the
*busiest* people alive though...


-- 
		-harry

Harry Halpin,  University of Edinburgh 
http://www.ibiblio.org/hhalpin 6B522426

Received on Thursday, 7 September 2006 22:32:45 UTC