The KPN rules


PRThe 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 relationthen KR and KKR , after, will give youThe 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). 