Re: [isabelle] isabelle/jedit



On 8/10/2012 12:11 PM, Gergely Buday wrote:
Genuine interaction in interactive theorem proving is to be able to concentrate on the course of the proof without more than needed distraction of technicalities. I think menus could help this, you say they wouldn't, and they do not fit the picture. What other possibilites does jEdit have you refer to? - Gergely

Gergely,

To be content, it helps to know what else is out there, which might not be new news to you:

http://www.cs.ru.nl/~freek/comparison/comparison.pdf <http://www.cs.ru.nl/%7Efreek/comparison/comparison.pdf>

I found some others, so I have about 25 in my browser bookmarks.

Here's something that looked interesting:

http://naproche.net/

But then, it uses automatic theorem provers:

http://naproche.net/downloads/2009/emergingsystems.pdf

There's Lamports TLA+2:

http://research.microsoft.com/en-us/um/people/lamport/tla/tla2.html

There's http://zermelo.org/

The short of it is that jEdit, as a frontend running on Linux, Windows, and the Mac, is much better than everything else out there, even in its incomplete state.

That doesn't mean the others aren't useful to people. The frontend isn't everything, and someday people will be putting great frontends on a lot of the other proof assistants, so I predict.

It's a bunch of things: documentation, language syntax, the logic engine, the editor, support, funding, etc. From my research, Isabelle is the overall winner, but then, I like it's natural deduction foundation. Someone else might need something like Coq's logic, not that I know much about it all. I could decide tomorrow that all this isn't worth the effort. If I did, I'd go quietly. I can see that people are doing all they can right now.

Regards,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.