We have the following remarks:

- Although we generate the axiom succ(on(1, 3)) ≡ false for stack(1, **2), we do not put**
on(1, 3) into its delete list. This is because we can deduce init(on(1, 3)) ≡ false **from** Init as well. A fluent atom is put into the add or the delete list of an **action only if** this fluent atom's truth value is definitely changed by the action. See Section 5 for more details about how a STRIPS-like description is generated from successor state axioms.
- **As one can see, our CCP procedure crucially depends on the fact that each type has**
a finite domain so that all reasoning can be done in propositional logic. This is a limitation of our current system, and this limitation is not **as bad as one might think.** First of all, typical planning problems all assume finite domains, and changing the domain of a type in an action description is easy - all one needs to do is to change the corresponding type definition. More significantly, a generic action domain description can often be obtained from one that assumes a finite domain. In **our blocks world** example, the numbers "1", "2", and "3" are generic names, and **can be replaced by**
parameters. For instance, if we replace "1" by x and "2" by y in the above STRIPSlike description of stack(1, 2), we will get a STRIPS-like description for stack(**x, y**)
that works for any x and y**. We have found that this is a strategy that often works in**
planning domains.

## 4. Formal Semantics

The formal semantics of an action domain description is defined by translating it into a situation calculus causal theory of Lin (1995). We shall show that the procedure CCP given above is sound under this semantics.

This section is mainly for those who are interested in nonmonotonic action theories. For those who are interested only in using our action description language for describing action domains, this section can be safely skipped.

We first briefly review the language of the situation calculus.

## 4.1 Situation Calculus

The language of the situation calculus is a many sorted first-order language. We assume the following sorts: situation for situations, action for actions, fluent **for propositional fluents,** truth-value for truth values true and false, and object **for everything else.**
We use the following domain independent predicates and functions:

- Binary function do - for any action a and any situation s, do(a, s**) is the situation**
resulting from performing a in s.

- Binary predicate H - for any p and any situation s, H(p, s) is true if p **holds in** s. - Binary predicate Poss - for any action a and any situation s, Poss(a, s**) is true if** a is possible (executable) in s.

- Ternary predicate Caused - for any fluent atom p, any truth value v**, and any situation**
s, Caused(p, v, s) is true if the fluent atom p **is caused (by something unspecified) to**
have the truth value v **in the situation** s.