Epistemic Rules

PR

The 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 'does not know that not' formula asserted for the generated world

KR and KKR. You need to select two lines (one a known formula and the other a suitable Eaccess relation

then KR and KKR , after, will give you

The implementation here is giving you two rules in one. The KR rule gives you that the proposition holds in the new world, and the KKR rule gives you that the agent knows it in the new world.

KTR. You select a known formula and the rule gives you the body of the known formula asserted for the same world as that of the known formula

TrKR. You select a formula that one agent knows that another agent knows and the rule gives you that the first agent knows that formula. The rule KTR ('anything that is known is true') also applies here, so the implementation gives you that as well, You get two lines, one from TrKR and the other from KTR (KTR justifies the first line displayed here and TrKR the second).