You might want to consider implementing import/export of OpenTheory proofs (
http://www.gilith.com/research/opentheory/) to get access to some larger
existing proofs. It would be interesting to see how they would look in the
web interface.
On Mon, Apr 23, 2012 at 3:32 AM, Cris Perdue <[email protected]> wrote:
> 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
>
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
