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.