Problems in formal temporal reasoning

摘要

Ever since its introduction by McCarthy and Hayes in 1969, the so-called frame problem has been the object of much fascination and debate. Although it was defined in the narrow context of the situation calculus, a specific temporal formalism, it was clear from the start that it is in fact a manifestation of some fundamental problem in temporal reasoning.Our aim in this informal paper is to identify the general form of certain classes of problems that arise in formal temporal reasoning. We argue that problems such as the frame problem arise from the conflicting desires to reason both rigorously and efficiently about the future. This conflict does not depend on the particular underlying temporal formalism. In particular, we identify two formalism-independent problems, called the qualification problem and the extended prediction problem, which subsume the frame problem. To illustrate the fact that these problems are indeed inherent to the prediction task and not to a particular formalism, we show that they arise in two distinct frameworks: classical mechanics, and Hayes' histories notation.