search

wo / tpg

Tree Proof Generator
GNU General Public License v3.0
151 stars 20 forks source link

Top and bottom constants #17

Open Lev135 opened 2 years ago

Lev135 commented 2 years ago

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 commented 2 years ago

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 commented 1 year ago

@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."