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
To be content, it helps to know what else is out there, which might not
be new news to you:
I found some others, so I have about 25 in my browser bookmarks.
Here's something that looked interesting:
But then, it uses automatic theorem provers:
There's Lamports TLA+2:
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and