We present a declarative formalization of STRIPS in the situation calculus. This section outlines its main components and features, at the same time that describes the structure of the paper.
First, we present a situation calculus formalization of the STRIPS representation of planning problems. This formalization is proposed in [7], and it is characterized by making the STRIPS database explicit and reifying the formulas that are in the database. This allows handling deletions, and quantifying over those formulas. Then, we describe the situations, actions, and strategy STRIPS uses to reason about those representations of planning problems. Instead of formalizing a reasoning strategy as a meta-theory of the object-theory describing a planning problem [3], we introduce the concepts of mental situations and mental actions as first order objects of the language. This allows us to formalize in a single theory the dynamics of both: (1) the object situations STRIPS reasons about, which describe a particular planning problem; and (2) the mental situations it constructs to reason about that problem.
The formalization of the reasoning strategy used by STRIPS (goal stack planning) is presented in two stages. First, we define the space of mental situations on which that reasoning strategy operates. The formalization of mental situations makes the goal stack explicit, and represents subgoals as reified formulas describing the formulas that should and should not be in the database associated with a given situation. The reasoning process performed by STRIPS is explained in terms of a single type of mental action, Hyp(a), which denotes the mental act of hypothesizing the execution of action a at a particular point of the plan currently being constructed. Later on in the paper, we introduce backtracking actions which allow retracting wrong hypotheses about actions. Then, we describe the heuristics and search strategy STRIPS uses to explore the space of mental situations. In particular, we provide axiomatizations of: (1) depth first search (with backtracking); and (2) some of the heuristics used by STRIPS for selecting actions and detecting dead-ends during the searching process. [15] shows how this simple formalization accounts for the standard STRIPS solution to the blocks world problem known as Sussman's anomaly. The successive mental situations constructed by STRIPS in the process of searching for that solution, and the interaction between such mental situations and the object situations (hypothetical solutions) they reason about are described in detail.
The ideas about the formalization of individual concepts and propositions in [6] are used to distinguish between the fact described by a formula and its truth value. In particular, we use a reified formula to represent the fact described by a formula, and the predicate True to assert the fact described by that formula. Thus True(p) is true iff the fact described by the reified formula p is true. We use two subsorts of variables for reified formulas: f for formulas in the database; and g for formulas in the goal stack.