Programming Language and Style.

We considered Prolog, Mercury, Haskell, Java and C++ but wrote the TWB in OCaml because it is a functional language with a large number of third party libraries. Functional languages are more concise than languages like C or Java, and functional programs are therefore easier to maintain and more resistant to memory management problems and runtime errors. OCaml also has a broad community of users, many third party libraries and has already been used to implement other successful generic theorem provers like Coq, Hol light and NuPrl. OCaml is an hybrid language which mixes elements of imperative programming with its functional basis. To minimise coding errors and reduce maintenance time, the TWB core infrastructure uses a purely functional style. But to avoid some of the ensuing performance penalties, a number of data structures use imperative programming style. Currently the TWB runs on modern operating systems such as Gnu/Linux and MacOsX. Moreover, the TWB has virtually no dependencies on third-party software outside the OCaml compiler itself, making it easy to install and port to other platforms. Why not just use Isabelle? Surely you can do all this sort of stuff in any logical framework? We actually received a review for one of our papers which claimed that most of the TWB could be built within Isabelle in one afternoon's work. Yes, you can use Isabelle, and yes, you can build the whole of the TWB inside Isabelle or any other logical framework. But try it and you will soon see that what you get is an extremely slow behemoth which will not run at an acceptable speed. For example, just the various pattern matching and rewriting principles built into the TWB rule syntax will be hard enough. The reason is that Isabelle is too big a hammer for the nail we have. There is no need for all of the higher order machinery that comes for free with Isabelle. Ideally we want to turn off interaction and have the TWB find closed tableau automatically. So you will end up having to program tactics and tactical on top of the Isabelle version of the TWB anyway. Finally, Isabelle does not compile down to a stand alone program for the tableau calculus that you have designed. We challenge anyone that belives they can mimic the TWB in Isabelle (or any other logical framework) to try it and report back to us. In particular, please try to log the time it took you and record the run times for your prover for modal logic K and S4 say on our examples from the "demo" page.