Epistemic modal logic was invented by Finnish philosopher Jaako Hintikka to represent knowledge and belief (in a book published in 1962), and is now used by computer scientists to model and design systems of autonomous software agents. It uses modal operators to indicate which propositions are known to which agents.
A common modal system for beliefs is C. I. Lewis‘ system S5, which (among other axioms) assumes that agents know what it is they know (positive introspection) and know what it is that they don’t know (negative introspection). (In other words, if an agent does not know whether or not some proposition is true, then the agent knows that he does not know whether or not that proposition is true). These are quite strong assumptions, and have been criticized as being unrealistic. Two computer scientists, Joseph Halpern and Leandro Chaves Rego, have now identified negative introspection as the axiom which makes the satisfiability problem for S5 NP-complete.
As an aside, discussion of positive and negative introspection by epistemic logicians meant that they fully understood Donald Rumsfeld’s statements about known unknowns vs. unknown unknowns.