Similarly, we have the following axiom about Caused(F, false, do(A, S)):

 $$\frac{1}{2}$$  $$\frac{1}{2}$$  . 
Caused(F, false, do(A, S)) ≡ H(φ1, S) ∨ · · · ∨ H(φm, S) ∨
H(φ
′
1, do(A, S))**∨ · · · ∨** H(φ
′
k, do(**A, S**)).

From these two axioms and (8), we get:

$$H(F,do(A,S))\equiv H(\varphi_{1},S)\vee\cdots\lor H(\varphi_{n},S)\vee$$ $$H(\varphi_{1}^{\prime},do(A,S))\vee\cdots\lor H(\varphi_{l}^{\prime},do(A,S))\vee$$ $$H(F,S)\wedge\neg[H(\phi_{1},S)\vee\cdots\lor H(\phi_{m},S)\vee$$ $$H(\phi_{1}^{\prime},do(A,S))\vee\cdots\lor H(\phi_{k}^{\prime},do(A,S))].$$

Since M is a model of Comp(T ), M **satisfies the above formula. By the construction of**
MS,A**, it satisfies the pseudo-successor state axiom (1).**
Finally, the fact that MS,A is a model of Succ**1 should be apparent.** ✷
In general, (6) does not imply (7). There are several reasons:

- **As we mentioned after the procedure CCP, we assume that all information about the**
initial situation is given by **Init**.

- **Our procedure works on actions one at a time. The situation calculus theory** T
captures the effects of all actions in a single theory. So it is **possible that a bad specification of an action causes the entire theory to become inconsistent. For instance,** if we have Causes(true, p), Precond(A, true), and Effect(A, false, p), then the corresponding situation calculus theory will be inconsistent because of action A**. But for**
our procedure, it will generate an inconsistent theory only on A.

## 5. An Implementation

Except for Step 2.2, the procedure CCP in Section 3 is straightforward to implement. This section describes the strategy that our system uses for implementing Step 2.2. The main idea comes from the work of Lin (2001a) on strongest necessary and weakest sufficient conditions.

Given a propositional theory T, a proposition q, and a set B **of propositions, a formula**
ϕ is said to be a sufficient condition of q on B under T if ϕ **consists of propositions in** B and T |= ϕ ⊃ q. It is said to be the weakest **sufficient condition if for any such sufficient**
condition ϕ
′**, we have that** T |= ϕ
′ ⊃ ϕ. Similarly, a formula ϕ **is said to be a necessary**
condition of q on B under T if ϕ consists of propositions in B and T |= q ⊃ ϕ**. It is said** to be the strongest **necessary condition if for any such necessary condition** ϕ
′**, we have that**
T |= ϕ ⊃ ϕ
′.

It is easy to see that the weakest sufficient condition and the strongest necessary condition are unique up to logical equivalence under the background theory. It was shown (Lin, 2001a) that these two notions are closely related, and can be **computed using the technique**
of forgetting (Lin & Reiter, 1994a). In particular, for action theories, an effective strategy is to first compute the strongest necessary condition, add it to the background theory,