Review of K Propositional Rules

Logical System

There are the ordinary (non-modal) tree propositional rules plus

The Modal Negation (MN) rules



◊ 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