The Tableau WorkBench (TWB)

Last week I've started working toward the new sequent interface. After a bit of brainstorming I've soon realized that to implement the new frontend I've to change the way I handle generic data types in the TWB.

At the moment generic data types (for example how formulae are represented) are barried inside the TWB library, making very painful for the user to add a new datatype or a new container (for example a queue of tuples). Decoupling my generic types from the TWB library is conceptually easy, but technically complicated because of the ocaml type system.

This week I've re-learned about polimorphic variants and read a number of paper from Jacques Garrigue

During the second week I've finished off the macosx packaging, submitted patches, etc. I've also done a bit more work on the TWB debian package, but I'm still not happy with it.

Since the TWB is not yet ready for prime time, I've decided to build a small static demo of few calculi that I've implemented, namely K, KT, S4, PLTL and UB. My plan to to create a rich web client to display the tree generated by the tableau procedure and give the user a nice interface to nagivigate it.

Since that would require a fair bit of work, I've started with something very simple. The static demo allows you to select you logic from a list of 5 and to input a formula to test.

I've submitted my dissertation and finally I've some time to
spend on the TWB, website, tools, etc. During the next six months I'll try to make the TWB a product (from a project) and hopefully build a user base. I don't expect wide adoption, but I hope somebody, somewhere will start using it.

This diary is for work purposes and to keep track of ideas that might be useful along the track.

Ok, during the first week I've worked to re-write the configure script of the TWB. I've adopted automake and autoconf and used few custom rules written appositely to work with Ocaml projects. For reference I'm using a modified version of this configure.in: