- From: Dan Connolly <connolly@w3.org>
- Date: Sun, 5 Mar 2006 07:55:41 -0600
- To: Dan Connolly <connolly@w3.org>
- Cc: www-archive+breadcrumbs@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. 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