- From: <jos.deroo@agfa.com>
- Date: Thu, 7 Sep 2006 22:56:08 +0200
- To: connolly@w3.org
- Cc: Harry Halpin <hhalpin@ibiblio.org>, Sandro Hawke <sandro@w3.org>, www-archive@w3.org
Dan, > Jos, > > I seem to recall you supervised some work on turning Euler > proofs into running code, a la the curry/howard isomorphism. > > I found a pointer to one thesis... > > For Rew's information, Guido Naudts also wrote about > that anti-looping technique in his masters thesis > http://www.agfa.com/w3c/2002/02/thesis/thesis.pdf > > -- http://lists.w3.org/Archives/Public/www-archive/2004Jan/0069.html > > 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 :-) (I think he argued "is PhD level work" or something like that) In our actual work (and there is a PhD student involved who just went back to his home university in Halifax Canada after spending the last 3 months with us in Ghent Belgium) 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). In that way we hope to resolve "the machine doing things (*) that I know the computer could do for me" :-) (*) like writing running rules (and they really run :-)) > Do you remember if you sent me a pointer to work in progress > or something? > > Harry and just had an interesting discussion about semantic > web proof, and I told him I'd give him a pointer. > > Harry, I found a few other relevant bits while I was looking: > > Explanations and Proof-Language Meeting, Follow-Up > Date: Tue, 29 Apr 2003 22:44:32 -0400 > http://lists.w3.org/Archives/Public/www-archive/2003Apr/0069.html > > > proof representation noodling, cwm, euler > 25 Mar 2003 01:56:49 -0600 > http://lists.w3.org/Archives/Public/www-archive/2003Mar/0062.html > and Jos's reply > http://lists.w3.org/Archives/Public/www-archive/2003Mar/0070.html > > My more recent noodling is in public-cwm-talk: > > Re: struggling to understand the cwm/N3/reasons proof checking algorithm > http://lists.w3.org/Archives/Public/public-cwm-talk/2006JulSep/0009.html > > That thread is mostly me talking to myself; it started back in June: > > struggling to understand the cwm/N3/reasons proof checking algorithm Dan > Connolly (Wednesday, 7 June) > http://lists.w3.org/Archives/Public/public-cwm-talk/2006AprJun/0021.html > > Ah... and right near there, I see work on N3/turtle grammar stuff: > a notation3 grammar in XML formal grammar notation / EBNF Dan Connolly > (Friday, 16 June) > http://lists.w3.org/Archives/Public/public-cwm-talk/2006AprJun/0032.html > > > In a couple cases, my noodling got sufficiently organized that I > wrote a blog entry: > > bnf2turtle -- write a turtle version of an EBNF grammar > Submitted by connolly on Fri, 2006-02-10 > > http://dig.csail.mit.edu/breadcrumbs/node/85 > > > Investigating logical reflection, constructive proof, and explicit > provability > Submitted by connolly on Thu, 2006-02-16 > http://dig.csail.mit.edu/breadcrumbs/node/89 > > > We also talked about the state of the art in N3 semantics specification, > Harry. > > TimBL has a draft: > > $Revision: 1.17 $ of $Date: 2005/12/21 20:12:28 $ > http://www.w3.org/DesignIssues/N3Logic > > I sketched something: > > N3 Syntax and Semantics > http://dig.csail.mit.edu/2006/Papers/TPLP/n3absyn.html > > 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! > I think we haven't gotten an acceptance nor rejection notice. > > -- > Dan Connolly, W3C http://www.w3.org/People/Connolly/ > D3C2 887B 0F92 6005 C541 0875 0F91 96DE 6E52 C29E -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 7 September 2006 20:56:43 UTC