×

Nonmonotonic logic and temporal projection. (English) Zbl 0654.68107

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 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. 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. D. Harel, First-order dynamic logic (Lect. Notes Comput. Sci. 68) (1979; Zbl 0403.03024)], also with variations admitting an explicit time [cf. H. Andréka, I. Németi and 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.
Reviewer: M.Suchenek

MSC:

68T99 Artificial intelligence
03B60 Other nonclassical logic
03A05 Philosophical and critical aspects of logic and foundations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Charniak, E., Motivation analysis, abductive unification, and non-monotonic equality, Artificial Intelligence; Charniak, E., Motivation analysis, abductive unification, and non-monotonic equality, Artificial Intelligence
[2] Clark, L., Negation as failure, (Gallaire, H.; Minker, J., Logic and Databases (1978), Plenum Press: Plenum Press New York), 293-322
[3] Davis, M., The mathematics of non-monotonic reasoning, Artificial Intelligence, 13, 73-80 (1980) · Zbl 0435.68075
[4] Etherington, D. W., Formalizing non-monotonic reasoning systems, (Computer Science Tech. Rept. No. 83-1 (1983), University of British Columbia: University of British Columbia Vancouver, BC) · Zbl 0638.68100
[5] Etherington, D. W.; Reiter, R., On inheritance hierarchies with exceptions, (Proceedings AAAI-83. Proceedings AAAI-83, Washington, DC (1983)), 104-108
[6] Goebel, R. G.; Goodwin, S., Applying theory formation to the planning problem, (Research Rept. CS-87-02 (1987), Logic Programming and AI Group, Department of Computer Science, University of Waterloo: Logic Programming and AI Group, Department of Computer Science, University of Waterloo Waterloo, Ont)
[7] Hanks, S.; McDermott, D., Temporal reasoning and default logics, (Computer Science Research Rept. No. 430 (1985), Yale University: Yale University New Haven, CT)
[8] Hanks, S.; McDermott, D., Default reasoning, nonmonotonic logics, and the frame problem, (Proceedings AAAI-86. Proceedings AAAI-86, Philadelphia, PA (1986)), 328-333
[9] Hayes, P. J., The second naïve physics manifesto, (Hobbs, J. R.; Moore, R. C., Formal Theories of the Commonsense World (1985), Ablex: Ablex Norwood, NJ), 1-36
[10] Joshi, A.; Webber, B.; Weischedel, R., Default reasoning in interaction, (Proceedings of the Non-Monotonic Reasoning Workshop (1984)), 141-150
[11] Kautz, H., The logic of persistence, (Proceedings IJCAI-85. Proceedings IJCAI-85, Los Angeles, CA (1985)), 401-405
[12] Lifschitz, V., Formal theories of action, (Brown, F., The Frame Problem in Artificial Intelligence: Proceedings of the 1987 Workshop (1987), Morgan Kaufman: Morgan Kaufman Los Altos, CA) · Zbl 0718.68019
[13] Lifschitz, V., Pointwise circumscription: Preliminary report, (Proceedings IJCAI-85. Proceedings IJCAI-85, Los Angeles, CA (1985)), 406-410
[14] Lifschitz, V., Some results on circumscription, (Proceedings of the Non-Monotonic Reasoning Workshop (1984)), 151-164
[15] Loui, R.P., Response to Hanks and McDermott: Temporal evolution of beliefs and beliefs about temporal evolution, Cognitive Sci.; Loui, R.P., Response to Hanks and McDermott: Temporal evolution of beliefs and beliefs about temporal evolution, Cognitive Sci.
[16] McCarthy, J., Circumscription—a form of non-monotonic reasoning, Artificial Intelligence, 13, 27-39 (1980) · Zbl 0435.68073
[17] McCarthy, J., Applications of circumscription to formalizing common sense knowledge, (Proceedings of the Non-Monotonic Reasoning Workshop (1984)), 295-324
[18] McCarthy, J.; Hayes, P. J., Some philosophical problems from the standpoint of artificial intelligence, (Meltzer, B.; Michie, D., Machine Intelligence, 4 (1969), Edinburgh University Press: Edinburgh University Press Edinburgh), 463-502 · Zbl 0226.68044
[19] McDermott, D. V., A temporal logic for reasoning about processes and plans, Cognitive Sci., 6, 101-155 (1982)
[20] McDermott, D. V., Nonmonotonic logic II: Nonmonotonic modal theories, J. ACM, 29, 1, 33-57 (1982) · Zbl 0477.68099
[21] McDermott, D. V.; Doyle, J., Non-monotonic logic I, Artificial Intelligence, 13, 41-72 (1980) · Zbl 0435.68074
[22] Perlis, D.; Minker, J., Completeness results for circumscription, (Computer Science Tech. Rept. TR-1517 (1985), University of Maryland: University of Maryland College Park, MD) · Zbl 0589.03021
[23] Poole, D., On the comparison of theories: Perferring the most specific explanation, (Proceedings IJCAI-85. Proceedings IJCAI-85, Los Angeles, CA (1985)), 144-147
[24] Reiter, R., A logic for default reasoning, Artificial Intelligence, 13, 81-132 (1980) · Zbl 0435.68069
[25] Shoham, Y., Time and causation from the standpoint of artificial intelligence, (Computer Science Research Rept. No. 507 (1986), Yale University: Yale University New Haven, CT)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.