- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 07 Sep 2006 13:23:12 -0500
- To: Harry Halpin <hhalpin@ibiblio.org>, Jos De Roo <jos.deroo@agfa.com>
- Cc: www-archive@w3.org, Sandro Hawke <sandro@w3.org>
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. 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 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
Received on Thursday, 7 September 2006 18:23:32 UTC