Can an agent that possesses specific knowledge about the world be said to know all the consequences of that knowledge? Given that the process of determining whether a given statement is a consequence of the premises can require extensive computation, it seems reasonable to assert that the agent does not know a given fact just because it is a logical consequence of what the agent consciously knows. The aim of this paper is to provide a formalism that in some sense stratifies an agent’s knowledge based on how complex the reasoning required to arrive at the conclusion is.

The author does this by describing a set of depth-bounded approximations to Boolean logic. The zero level of this hierarchy makes use of a three-valued logic--known true, known false, and status unknown. The author describes a proof process called interim proofs, and shows that whether a statement that a formula is a consequence of a set of hypotheses is level-0 refutable can be decided in time bounded by the square of the number of occurrences of symbols in the formula and the hypotheses.

A hierarchy is obtained by allowing the manipulation of virtual information, that is, information that one does not actually possess, but that is temporarily assumed. The depth is essentially the number of such assumptions that are made to construct the proof. The author shows that at each level the decision problem as to whether a refutation is possible at that level is polynomial time.