Otherwise, the action A's effect on F **is indeterminate. In this case, output two** axioms:

$$\begin{array}{l}{{s u c c(F)\supset\alpha_{F},}}\\ {{\beta_{F}\supset s u c c(F),}}\end{array}$$

where αF is a strongest formula satisfying the first implication, and βF **a weakest**
formula satisfying the second implication. In the following, to be explicit about the action A **for which we are computing its effects, we will write the axioms as**
SuccA, InitA, and **Succ**1A.

Conceptually, Step 2.1 in the above procedure is most significant. In the next section, we shall prove that this step is provably correct under a translation to the situation calculus causal theories of Lin (1995). Computationally, Step 2.2 is **the most expensive. We shall**
describe the strategies that our system uses to implement it **in Section 5.**
For this procedure to work properly, the action domain description should satisfy the following conditions.

1. We require that all fluent atoms in Init, Succ, and Succ**1 be among those generated**
in Step 1. This would rule out cases like Fluent(on(x, y), block(x)∧ **block**(y) ∧ x 6= y)
together with Defined(clear(x), ¬∃(y, block)on(y,x**)), as the latter would generate**
fluent atoms of the form on(x, x**) which are ruled out by the fluent definition for** on. Here one could either drop the inequality constraint in the definition of on **or change**
the complex fluent definition into Defined(clear(x), ¬∃(y, block)(on(y,x) ∧ x 6= y)). We could have built in a test in our procedure above to reject an action domain description with incoherent fluent definitions like this. One easy way of making sure this does not happen is not to use inequality constraints in the definition of fluents.

2. As we mentioned above, for each action there should be exactly one action precondition that captures exactly the conditions under which the **action is executable.**
When the action precondition is given explicitly like this, **one needs to be careful** in writing action effect axioms and domain rules so that no contradictory effects would be generated. For instance, given Precond(A, true**), the action effect axioms** Effect(A, true, F) and Effect(A, true, ¬F**) are clearly not realizable simultaneously.** Similarly, if Causes(true, F**) is given as a domain rule, then one should not write the** effect axiom Effect(A, true, ¬F). Had we not insisted that A **be always executable, we**
could simply conclude that A **is not executable when its effect axioms are in contradiction or when some of its effect axioms contradict domain rules. It remains future**
work to extend our procedure to allow for automatic generation of these implicitly given action preconditions. For now, we shall assume that the given action domain specification is consistent in the sense that for each action instance A **generated in** Step 1, the following theory Init ∪ Succ ∪ Succ1 ∪ {init(ϕ) ⊃ ¬**succ**(F) |

$\therefore(A,\varphi,\neg F)$ is a g
Effect(A, ϕ, ¬F**) is a ground instance of effect axiom**}