Nonmonotonic logic and temporal projection (Q1108819)

The reviewed article is a revised version of the paper that won the AI Journal Best Paper Award at AAAI-86. It addresses the following ``temporal projection problem'' (p. 385\({}^{17-20}):\) ``[...] given an initial description of the world [...], the occurrence of some events, and some notion of causality [...], what facts are true once all the events have occurred?'' The authors investigate an instance of this problem. They express the notions involved in the problem using a three-sorted, first-order language with constants, unary function `result', and two predicate symbols: binary t and ternary ab. The constants denote `events', `descriptors' of the world, and `situations' (instances of the world). Function \(result:\quad events\times situations\to situations\) denotes the effect of occurrence of an event. Predicate t (truth) denotes the satisfaction relation between `descriptors' and `situations'. Predicate ab (abnormality) characterizes all triples \(<descriptor\), event, \(situation>\) for which `event' applied to `situation' causes `descriptor' ``to stop being true'' (p. 387 4) in the resulting situation. For example, result(LOAD,s) denotes the situation immediately after occurrence of event LOAD in situation s, t(LOADED,s) is true for exactly those s's which are LOADED, and ab(ALIVE,\(SHOOT,s)\) is true for exactly those s's which are ALIVE and whose \(result(SHOOT,s)\) are not. The authors provide arguments for their thesis that the following axiomatization (p. 387) (1) \(t(ALIVE,S_ 0)\) (2) \(\forall s.t(LOADED\), result(LOADED,s)) (3) \(\forall s.t(LOADED,s)\supset ab(ALIVE,SHOOT,s)\wedge t(DEAD\), result(SHOOT,s)) (4) \(\forall f\), e, s.t(f,s\(\wedge \neg ab(f,e,s)\supset t(f\), result(e,s)) does not entail all intuitively true properties of the situation \[ S_ 3=result(SHOOT,\quad result(WAIT,\quad result(LOAD,S_ 0)))\quad, \] under assumption of minimality of (the semantics of) ab. E.g., they claim (p. 390\({}^{12,13})\) that in a certain minimal model of (1)-(4), \(t(DEAD,S_ 3)\) is not satisfied. The authors use examples of predicate circumscription and default logic to illustrate a consequence of their thesis: any logic consistent with respect to minimal semantics of ab cannot prove all such properties. Moreover, the authors disagree with published suggestions directed at an earlier version of this paper. Because the paper is written with a consistent lack of preciseness its errors cause that the reader can only guess at the authors' intentions. Here are some examples of more serious errors. The definition (p. 382\({}_{12-3})\) of `extension' the authors attribute to Reiter is faulty: according to authors' version, Cn(\(\neg A)\) is an extension of the empty theory with default MA/\(\neg A\), while it is not in the sense of \textit{R. Reiter} [Artif. Intell. 13, 81-132 (1980; Zbl 0435.68069)]. The definition on page \(384_{15-13}\) does not define the predicate circumscription but the closed world assumption [cf. \textit{R. Reiter}, On closed world data bases. In: H. Gallaire and J. Minker (eds.), Logic and databases, Plenum Press, 55-76 (1978; Zbl 0412.68089)]. The lack of precise definition of situation seems to be the reason of existence of an unwanted minimal model for axioms (1)-(4), in which ab(LOADED,\(WAIT,s)\) is true for certain s. Consequently, the authors implicitly minimize the number of cases ab assumes the truth value in a sequence of situations instead of minimizing its semantics. It is a routine exercise to check that once the `situation' is defined as a pair \(<x,y>\), where x may be ALIVE or DEAD (but not both), and y may be LOADED or UNLOADED (but not both), axioms (1)-(4) do entail, assuming the minimality of ab, that situation \(S_ 3\) (defined above) has the attribute DEAD. (Actually, the argument on p. 389\({}_{9-6}\) in the authors' proof of the contrary is invalid.) On the other hand, the authors' suggestion that situations were ``point[s] of time'' (p. 387\({}^{19})\) would make the formalism they use senseless since in such a case function `result' would not depend on its first argument, and, making ab directly time-dependent, would contradict intuitive understanding of abnormality. Adequacy of axioms (1)-(4) is at least doubtful. E.g., (3) \& (4) \(+\) minimality of ab entail \(\forall s.t(LOADED,s)\supset t(ALIVE,s)\), which does not necessarily coincide with the authors' intentions. Closer scrutiny reveals that these axioms do not describe the problem correctly neither under temporal nor atemporal interpretation of situations. Taking all this into account, the authors' declaration that ``[...] the nonmonotonic logics [they] considered are inherently incapable of representing this kind of default reasoning'' remains, at best, unproved. Moreover, the ``temporal projection problem'' formulated in the reviewed paper is known in the area of programs' verification by name of partial correctness problem. It has been successfully expressed in the language of monotonic (ö) dynamic logic, cf. \textit{D. Harel}, First-order dynamic logic (Lect. Notes Comput. Sci. 68) (1979; Zbl 0403.03024)], also with variations admitting an explicit time [cf. \textit{H. Andréka}, \textit{I. Németi} and \textit{I. Sain}, Theor. Comput. Sci. 17, 193-218, 259-278 (1982; Zbl 0475.68009, Zbl 0475.68010)]. Therefore, the question whether this problem can or cannot be ``represented'' by means of one or another nonmonotonic logic is less dramatic than the authors seem to suggest.