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.