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

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.

http://plato.stanford.edu/entries/mathematics-constructive/

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Sunday, 5 March 2006 13:55:55 UTC