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.

The proper solution is to give a different semantic for the * operator in term of a least fix point. Therefore the tactic * now always succeed. To this end, I've introduced a generic mu operator, so now the repeat is interpreted as

` repeat t = mu \x . !(t ; \x | Skip)`

where Skip is the tactic that always succeed and ! is an operator that select the first successful tactic in an alternation.

So, to conclude, now the tactic for modal logic K is specified as

` ((Id|Or|And)* ; K)* `

that is then expanded to

` mu \x . ((mu \y . ( (Id|Or|And); \y | Skip )) ; K) ; \x | Skip ) `

Hopefully this will now make it easier for me to specify more complex tactic.