I would like to announce the Prooftoys visual proof assistant, a work in progress, and invite experimental use of it, available at http://prooftoys.org/.
The Prooftoys logic is very close to Peter Andrews' Q0, including essentially the same axioms and the same single fundamental rule of inference, Rule R, which allows replacement of a term by an equal term. The implementation builds up numerous derived rules of inference, which are available in the same way as theorems and the primitive rule of inference through the web-based user interface. Prooftoys and its user interface normally run entirely within the user's web browser for interactivity and immediate access. It includes an interactive proof editor, with ability to save and restore proofs to textual format. It supports inference in the style of natural deduction, using hypotheses. The system aims to make higher-order logic more accessible conceptually and easier to use as a tool, bringing more people to understand and use it. The implementation is very much a work in progress in all dimensions, but has been working well for experimental interactive use. It has a set of axioms for real numbers and some rather primitive derived rules of inference so it is possible to experiment with real numbers. More information is available on the Prooftoys <http://prooftoys.org/> web site. Best regards, Cris Perdue
------------------------------------------------------------------------------ For Developers, A Lot Can Happen In A Second. Boundary is the first to Know...and Tell You. Monitor Your Applications in Ultra-Fine Resolution. Try it FREE! http://p.sf.net/sfu/Boundary-d2dvs2
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
