Logical System
There are the ordinary (non-modal) tree propositional rules plus
The Modal Negation (MN) rules
plus
◊ R world, k, must be new [here the computer will choose for you]. The rule gives you two lines. It gives you access to the world it generates and it gives you the body of the modal possible formula asserted for the generated world
□ R , before, you need to select two lines (one a modal necessary formula and the other a suitable Access relation
then □ R , after, will give you
