A critical bug !!!

I've spent the last 10 days fighting with a nasty bug in the tactic component of the TWB. The problem was that I didn't implement the semicolon ";" operator in the strategy correctly. after a bit of pain an sweat, I finally managed to fix this problem, that btw affects the "stable" version of the TWB as well, and now I should be back on track to work on the sequent interface and all the old new feature that I had planned.

By fixing this problem I've also realized that I can express a more general fixpoint operator in the TWB. Up until now the strategy for modal logic K was specified by ((Id|Or|And)* | K)* where the star operator means "repeat until impossible" . However, the semantic of the star operator also implied that when no more rule are applicable, the strategy should fail. Coupling a failing strategy with the alternation operator "|" would always lead to an erroneous answer. By accident, and by mistake, I've managed to make this work anyway.

new support data structures (towards a sequent interface)

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

Second Week, more packaging and javascript

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.

First Week, first entry

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

Syndicate content