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
This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:32:49 UTC