Next: Complexity and the lack Up: Reasoning about algorithmic knowledge Previous: Logics of algorithmic knowledge   Contents

Knowledge and complexity

We have introduced the concept of algorithmic knowledge in order to represent not only what agents know or can know, but also how long they need to know what they can know. Our analyses up to now can only answer the first question. By means of the systems presented so far one can infer formulae of the form , but no definite statements of the form or . However, to decide if an agent can solve a problem under certain constraints, it is necessary to compute the exact amount of time he needs to solve that problem.

To answer the the How long''-question, a complexity analysis is needed. The underlying idea is simple. The complexities of many reasoning problem classes are well-known and can be computed at a low cost. (Complexities are typically, but not necessarily, measured by functions of the input size.) Since the average computation speed of an agent can be assumed to be constant, the amount of time he needs to solve some problem can be computed on the basis of the complexity function for the problem's class5.4.

Suppose that any formula in a class can be computed at the cost , where is the length of . Let be a constant number that measures the computation speed of an agent . If and if agent is able to infer , then it can be inferred that is able to compute within time units. That is, can be assumed to be true. So, by the aid of complexity theory we can obtain epistemic principles for specific problem classes.

We shall not make any assumption about the nature of the complexity measures and develop our logics independent of the complexity theory in use. We calculate the cost of computing a formula of the language by way of cost functions, which are agent-dependent, partial funtions from to the set of natural numbers. That is, a cost function is defined for each agent . Intuitively, is the number of time units needed by to decide on the basis of all what he knows. Such a cost funtion is defined on the basis of known complexity functions for specific problem classes which can be expressed in the language. Clearly, is defined only for certain sets of formulae, namely for those formulae whose complexities are known. The agents' computation speed and the details how the complexity of a certain formula is measured are encapsulated in the specification of the cost function.

If a cost function is defined for a formula, then certain epistemic statements concerning that formula can be made. If the formula can be inferred reliably by the agent , then the amount of time needed to infer it is , so can be assumed to be true. Whether or not can be inferred reliably by , the introspective knowledge of that can be established after time units, because his computation of will return a positive or negative answer after at most time units. Therefore, and are valid. Those axioms will be added to the systems of algorithmic knowledge examined earlier to make more powerful logics for resource-bounded reasoning.

The complexity analysis makes it possible to prove many unconditional, definite epistemic sentences of the form . Let be a propositional tautology and let be defined. Applying the rule (NEC) yields the theorem . Hence, can be derived, by (AC1).

The main task in specifying a system of algorithmic knowledge with complexity analysis is to define the cost functions for the language . Let us consider how such cost functions can be constructed. We have argued in section 5.2.1 that if is provable then can be inferred. We have posed the question if natural number can be determined such that the stronger sentence can be assumed as a postulate. It is not yet known whether or not the provability problem for K is decidable, so we restrict our attention to certain subclasses. Let be an objective formula. Then it can be decided in time , as we know from complexity theory. If an agent is able to recognize objective formulae and to select a special procedure to compute them, he can derive reliably each objective tautology in a time proportional to .

Interestingly, the previous analysis can be used by an agent within the system in order to reason about himself or about other agents, provided that he has a built-in mechanism to calculate the complexity of reasoning problems. (Such a mechanism can be adopted easily by an agent.) Assume that an agent tries to find out how long agent will need to infer a formula if he chooses to. It is plausible to assume that can recognize relatively easily that belongs to the class of objective formulae, so he can reason about agent exactly like we did before to find out that the time agent needs is proportional to . Generally, does not know 's computation speed. However, he may obtain that information from external sources or through his own observations. If knows the computation speed of , he will be able to compute the amount of time needed by to infer . In other words, he can calculate for any objective formula . But to estimate the time would need to derive , agent does not have to actually derive it. He has only to recognize the class that belongs to and then to calculate the complexity of , which can be accomplished in linear time. So is a plausible postulate, where is the computation speed of .

Hence, the definition of the complexity function for may include the following clauses: for all objective formulae

• for all and all agents

The complexity of the decision procedures for normal modal logic has been investigated extensively ([HM92].) It has been shown (cf. theorem 28) that modal epistemic logic can be embedded faithfully to our systems of algorithmic knowledge, i.e., there is a fragment of the language which can be translated one-to-one to modal logic. Consequently, the complexity results obtained for normal modal logic can be applied to determine the cost of solving problems which can be formalized in that fragment. In that way the cost function can be specified for that fragment.

Next: Complexity and the lack Up: Reasoning about algorithmic knowledge Previous: Logics of algorithmic knowledge   Contents
2001-04-05