There are the ordinary (non-modal) tree propositional rules plus
The Modal Negation (MN) rules
◊ S5 world, k, must be new [here the computer will choose for you]
□ S5 any world, stage 1, your choice
Review of Tree Propositional Rules, shown as patterns
Here the letters 'P' and 'Q' are being used to stand for entire well formed formulas (so, on a particular occasion, 'P' might stand for the atomic formula 'F' and, on another occasion, it might stand for the compound formula 'F&G').