The following theorem shows that the procedural semantics given in the previous section is sound with respect to the semantics given here.

Theorem 1 Let D be an action domain description, and T **its translation in the situation**
calculus. Let A be any ground action instance, s a situation variable, and ϕ(s) **a situation**
calculus formula that satisfies the following two conditions (1) it contains at most the two situation terms s and do(A, s)**; and (2) it does not mention any predicate other than** H,
equality, and static relations. Let ϕˆ be obtained from ϕ by replacing each H(f, s) **in it by**
init(f), and each H(f, do(A, s)) in it by succ(f)**. Then**

$$s)\supset\varphi(s)$$
$\frac{x}{x}=\frac{1}{x+1}$ 2. 
comp(T ) |= ∀s.Poss(A, s) ⊃ ϕ(s**) (6)**
if Init ∪ Succ ∪ Succ1 |= ˆϕ, (7)
where Init, Succ, and Succ1 are the sets of axioms generated for A **according to the procedure in Section 3**
Proof: Suppose S is a situation and M is a model of comp(T ) ∪ {Poss(A, S)}**. Construct**
MS,A **as follows:**
- the domain of MS,A **is the object domain of** M.

- the interpretations of non-situational function and predicate symbols in MS,A **are the**
same as those in M.

- for any fluent atom f, MS,A |= init(f) iff M |= H(f, S) and MS,A |= succ(f**) iff**
M |= H(f, do(A, S)).
Clearly, M |= ϕ(S) iff MS,A |= ˆϕ. We show below that MS,A **is a model of the left hand**
side of (7). From this, we see that if (7), then (6).

Notice first that a ground fluent atom F is generated by the procedure CCP iff **Fluent**(F)
is true in M. Notice also that all fluent atoms in Init∪ Succ∪ Succ1 **must be generated by**
the procedure.

We show first that MS,A is a model of **Init**:

1. If Axiom(ψ) is a domain axiom, then ψ is in T . Thus M satisfies ψ. Since ψ **has no**
fluent symbols in it, MS,A **satisfies it too.**
2. If Causes(ψ, f(x1, ..., xn**)) is a domain rule, then**
(∀~ξ).Fluent(f(x1, ..., xn)) ⊃ (∀s){H(ψ, s) ⊃ Caused(f(x1, ..., xn)**, true, s**)}
is in T . Thus M **satisfies**
(∀~ξ).Fluent(f(x1, ..., xn)) ⊃ (∀s){H(ψ, s) ⊃ H(f(x1, ..., xn), s)}.

Thus if **init**(ψ
′) ⊃ init(F) is a corresponding formula in Init**, where** ψ
′ and F is some ground instantiation of ψ and f(x1, ..., xn), respectively, then Fluent(F**) must**
be true in M (otherwise the above formula would not be in Init), so M **satisfies** H(ψ
′, S) ⊃ H(F, S). By the construction of MS,A, it satisfies **init**(ψ
′) ⊃ init(F**). The**
case for Causes(ψ, ¬f**) is similar.**