How to Progress a Database II: The STRIPS Connection

Abstract

Ever since STRJPS was first introduced (Fikes and Nilsson [3]), its logical semantics has been problematic. There have been many proposals in the literature (e . ~. Lifschitz [4], Erol, Nau and Subrahmanian l2], Bacchus and Yang [1]). These all have in common a reliance on metatheoretic operations on logical theories to capture the add and delete lists of STRIPS operators, but it has never been clear exactly what these operations correspond to declaratively, especially when they are applied to logically incomplete theories. In this paper we provide a semantics for STRIPS-like systems in terms of a purely declarative situation calculus axiomatization for actions and their effects. On our view, STRJPS is a mechanism for computing the progression (Lin and Reiter [6], Pednault [8]) of an initial situation calculus database under the effects of an action. We illustrate this idea by describing two different STRIPS mechanisms, and proving their correctness with respect to their situation calculus specifications.