The following theorem states that all the defined systems DEK, DEK, DES4, and DES4 solve the logical omniscience problem. It says that none of the rules NEC, MON, and CGR is valid. Moreover, an agent's explicit knowledge at a time, i.e., the totality of all what this agent knows at that time, needs not be closed under any nontrivial logical rule.
An agent described by the given logics is not logically omniscient. On the other hand, we cannot say that he is not rational: the agent is rational, because he can (at least in principle) perform actions to close his knowledge under logical laws, as the following theorems show. Instead of the necessitation rule and monotony rule in modal epistemic logic we have now a theorem stating that the agents can know all classical theorems and can draw all consequences of what they know, provided that they perform the right reasoning.
Probably, the above rules and theorems are derivable for a larger class of formulae, not only for objective ones. The following list comprises some more provable formulae of DEK and its extensions. They say that if all premises of a valid inference rule are known, then after some steps of reasoning the agent will know the conclusion. This still holds if one of the premises is not known yet but will be known after some reasoning. The theorem is proved in appendix B.