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

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