| Main |
| F.A.Q. |
| References |
| Contact |
| Frequently Asked Questions |
| Main |
| F.A.Q. |
| References |
| Contact |
The following is the beginning of a FAQ for Belle. Right now, due to the age of the project, there hardly have been any questions about it, let alone frequently asked ones. Therefore the following reads more like a list of questions I hope will be asked. At least they give an introduction to the background of the project.
Belle is (well, will be) an generic higher order theorem prover, in the style of Isabelle. As such, it is a member of the LCF family of theorem provers and is, like Isabelle, not fixed to any particular logic, but rather tries to provide general support for a number of logics. One can also think of Belle and Isabelle each as being a family of closely related theorem provers.
Through my work the last year in the theorem proving group at the Technical University of Munich, I've been subjected to the internals of Isabelle, to the degree where I think I understand the system. More or less, anyway.
As my understanding has grown, so has my list of "things I don't understand about Isabelle" (I had a much longer list when I first started using Isabelle, but it was of somewhat different nature than my present one). My original reason for implementing a new version of Isabelle was simply to try and learn how such a thing is really built. After all, one thing is knowing enough to debug and extend an existing system, another thing is re-implementing it from scratch. By building a system myself, I would also better understand some of the design and implementation decisions taken for Isabelle, and thus I would ultimately better understand how to use and modify Isabelle, which is what I do for a living.
After discussing the possibilty of implementing a new system with my colleagues, it has become clear that, for all the good things in Isabelle, there is still room for improvements. This should not be any surprise, of course, since Isabelle has been evolving steadily since 1986, and with 20/20 hindsight, not all design or implementation decisions have been equally optimal. Implementing a new system will hopefully remedy the situation of some of the most problematic spots in Isabelle (and introduce some new ones).
Primarily, the logical kernel will be implemented by one person, me. Mainly, this is because nobody else has the time (nor the inclination) to help me implement it, and a close runner-up that I have strong opinions on how it should be implemented, and would rather do it myself, at least here in the beginning of the project. As for the rest of the system, I'm looking for all the help I can get.
Luckily, I'm not completely on my own; Apart from my colleagues in general, who continually point out trouble spots and give me feature requests for the new system, Gerwin Klein is actively helping me on design issues, particularly with the syntax module, and Farhad Mehta is helping out with the implementation.
If you are a user of Isabelle, you can help by sending me your praise for and grievances with Isabelle, so that I/we can take your comments into account when implementing Belle (you should, of course, also send such comments to the Isabelle mailing list).
For those who have no idea of what I am going on about, here are some links to existing systems, all thoroughly documented.