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.

I wonder if Rumsfeld worries about those unknown truths that are, in fact, unknowable…

http://plato.stanford.edu/entries/fitch-paradox/#1

The problem with Rumsfeld is that he believes in

positiveintrospection – the rule that Kp implies KKp. He lists known knowns, known unknowns, and unknown unknowns, but not unknown knowns. There are some things that one knows in such a way that one doesn’t even realize that one knows them (automatic presuppositions that are in fact true, for instance).Also, note that satisfiability for even simple propositional logic is NP-complete. When you add a modality it in general gets harder (PSPACE-complete in the case of S4, it seems), but adding negative introspection gets you back down to NP, so it really is a useful simplifying assumption, even though it’s clearly false. (Of course, if you believe something like what I said above, then even S4 is too strong, but it’s at least a better approximation.)