Top and bottom constants

[Lev135]

As I can see, there is no way to enter logical constants (I've tried top/bottom/0/1). Of couse, one can use p -> p for top, but it isn't convenient. Although constants are not very usefull in classical logic, they often occur in modal logic formulas.

[wo]

Yes, that's not supported at the moment. Do you have a reference to standard tableau rules for a language with top and bottom? Any branch with bottom or ~top is closed?

[Lev135]

@wo
Yes, from Fitting 2007 (Handbook of Modal logic, chapter 2):
"A tableau branch is called closed if it contains T Z and F Z for some formula Z, or
if it contains F \top, or T \botom. A tableau is closed if every branch is closed."