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

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