W3C home > Mailing lists > Public > www-archive@w3.org > March 2006

Re: Jape, sequents, and judgements (and constructive semantics)

From: Dan Connolly <connolly@w3.org>
Date: Sun, 5 Mar 2006 07:55:41 -0600
Message-Id: <11ca5ac61e46ae79dcd907a7b4177f98@w3.org>
Cc: www-archive+breadcrumbs@w3.org
To: Dan Connolly <connolly@w3.org>

On Feb 28, 2006, at 9:54 AM, Dan Connolly wrote:

>  I mentioned to Pat Hayes that we're starting to get some traction on 
> this semantic web proof checking stuff in the TAMI and PAW projects, 
> and he said I should check out Jape, a proof editor by Richard Bornat 
> and company. It's open source, with a user interface in Java and the 
> core engine in ocaml.

some older, related notes:

" Intuitionistic arithmetic can consistently be extended by axioms 
(such as Church's Thesis) which contradict classical arithmetic, 
enabling the formal study of recursive mathematics."
  -- http://plato.stanford.edu/entries/logic-intuitionistic/

However, the wider interpretations come at a cost: for example, when we 
pass from our initial, natural interpretation of P vel Q to the 
unrestricted use of the idealistic one, ¬(¬Pwedge¬Q), the resulting 
mathematics cannot generally be interpreted within computational models 
such as recursive function theory.


Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Sunday, 5 March 2006 13:55:55 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:32:49 UTC