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/
