## 5 Efficiency and Finity of Computations
This process begins with step 8, which finds the minimum requested time step, \(m\). If \(m\) is greater than the requested time horizon \(h\), then the iterations terminate (step 10) and the computation is finalized (steps 22-23). Step 10 ensures the finity of the returned trajectories and, correspondingly, of the computation. If \(m\leq h\), then step 10 removes from \(G\) the groundings of all rules that produce information about the state of the world at step \(m\) or greater. This is accomplished by setting the corresponding \(enabled(T)\) externals to false, which causes those rules to become inapplicable, and by releasing the externals. By releasing the externals, we ensure that, at steps 11 and 12, clingo will completely remove from \(G\) the groundings of all rules that have become inapplicable. ```
0:\(p\): pre-determined time steps, e.g., from observations and queries, as facts of the form \(time(t)\)
0:\(O\): a set of observations
0:\(h\): threshold for requests for the creation of new time steps
0: an answer set
1:\(\triangleright\) Expansion phase (\(base+timedep(0)+p+O\))
2:\(G\gets ground(base\cuptimedep(0)\cup p\cup O)\)
3: For every external \(enabled(t)\) from G, assert \(enabled(t)\) true via clingo's \(assign\_external()\)
4:\(A\leftarrow solve(G)\)
5:\(\triangleright\) end of expansion phase
6:while\(\{t\,|\,nevitine(t^{\prime},t)\in A\text{ and }time(t)\
ot\in A\}\
eq\emptyset\)do
7:\(\triangleright\) Retraction phase
8:\(m\leftarrow min\{t\,|\,nevitine(t^{\prime},t)\in A\text{ and }time(t)\
ot\in A\}\)
9: If \(m>h\) then exit while
10: For every external \(enabled(t)\) from \(G\) such that \(t\geq m\), assert \(enabled(t)\) false and release it via clingo's \(release\_external()\)\(\triangleright\) i.e., it is no longer an external
11:\(solve(G)\)\(\triangleright\) preparatory step for cleanup(0)
12:\(cleanup(G)\)
13:\(\triangleright\) end of retraction phase
14:\(\triangleright\) Expansion phase
15:\(G\leftarrow ground(\{time(t).\,|\,nevitine(t^{\prime},t)\in A\text{ and }time(t)\
ot\in A\})\)\(\triangleright\) add new time steps to the ground program
16:\(G\leftarrow ground(timedep(m))\)
17: For every external \(enabled(t)\) from \(G\) such that \(t\geq m\), assert \(enabled(t)\) true
18:\(A\leftarrow solve(G)\)
19:\(\triangleright\) end of expansion phase
20:endwhile
21:\(\triangleright\) addition of the output module
22:\(G\leftarrow ground(output)\)
23:return\(solve(G)\)
```  
**Algorithm 3** Algorithm _Incremental\({}^{h}\)  
It is important to note that this retraction phase is a _fundamental step_ in ensuring the satisfaction of the Module Theorem in _Incremental\({}^{h}\)_. Without the retraction phase, it is not difficult to see that rules triggered during the following expansion phase may yield (ground) literals that are already derived by rules triggered at earlier time steps. This phenomenon is due to the presence of durative aspects in the action descriptions. If the language is restricted to traditional inertial and default fluents, then the retraction phase is not necessary. Next, step 15 adds the requested time steps to \(G\). Step 16 adds to \(G\) the groundings of all rules that compute the state of the world at time steps \(m\) and later. Step 17 asserts all externals from \(G\) true and step 18 calculates the updated answer set \(A\) of \(G\). At this point, the algorithm verifies whether \(A\) contains any requests for new time steps and the process repeats. One may want to notice that steps 10 and 17 result in the enabling of all time steps \(t\geq m\), i.e., of all newly introduced time steps as well as every time step \(t\geq m\) that previously existed. The reason for enabling the latter set is that the retraction phase removes all information about the state of the domain at \(m\) and later time steps. During the following solving phase, the information must thus be recomputed. One may be tempted to think that this recomputation is unnecessary.