From: Harry Halpin <hhalpin@ibiblio.org>

Date: Thu, 07 Sep 2006 23:32:34 +0100

Message-ID: <45009E02.10803@ibiblio.org>

To: jos.deroo@agfa.com

Cc: connolly@w3.org, Sandro Hawke <sandro@w3.org>, www-archive@w3.org

Date: Thu, 07 Sep 2006 23:32:34 +0100

Message-ID: <45009E02.10803@ibiblio.org>

To: jos.deroo@agfa.com

Cc: connolly@w3.org, Sandro Hawke <sandro@w3.org>, www-archive@w3.org

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 6B522426Received on Thursday, 7 September 2006 22:32:45 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 7 January 2015 14:43:03 UTC
*