default

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').

∃D. The constant, a, must be new to the branch [here the computer will choose for you]

∀D. Any closed term, stage 1, your choice

∀D. Any closed term, stage 2, the constant 'a' chosen