Journal of the Association for Computing Machinery, Vol. 42, No. 2, March 1995, pp. 293–320.

Provably Correct Theories of Action

FANGZHEN LIN

AND

YOAV SHOHAM

Abstract. We investigate logical formalization of the effects of actions in the in the situation calculus. We propose a formal criterion against which to evaluate theories of deterministic actions. We show how the criterion provides us a formal foundation upon which to tackle the frame problem, as well as its variant in the context of concurrent actions. Our main technical contributions are in formulating a wide class of monotonic causal theories that satisfy the criterion, and showing that each such theory can be reformulated succinctly in circumscription.

Categories and Subject Descriptors. I.2.3[circumscription]; I.2.4[the situation calculus]

General Terms. Human Factors, Theory

Additional Key words and Phrases. Concurrent actions, the frame problem, reasoning about actions, temporal reasoning

Copyright 1995 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.