## 2 Preliminaries
External literals are declared by directives of the form:  
\[\#external\ l(\vec{x}):c_{1}(\vec{y_{1}}),c_{2}(\vec{y_{2}}),\ldots \tag{6}\]  
where \(\vec{x}\), and \(\vec{y_{i}}\)'s are sequences of ASP variables, \(l(\vec{x})\) is the (non-ground) literal being declared external, and \(c_{1}(\vec{y_{1}}),c_{2}(\vec{y_{2}})\) are a potentially empty set of conditions refining of which the subset of the ground instances of \(l(\vec{x})\) is to be declared external. For practical purposes, one can view the role of the elements of the directive to be similar to those of a rule of the form \(l(\vec{x})\gets c_{1}(\vec{y_{1}}),c_{2}(\vec{y_{2}})\), although of course an \(\#external\) directive has no bearing on the truth value of \(l(\vec{x})\). External declarations are convenient, in combination with \(assign\_external(l)\) and \(release\_external(l)\), for enabling and disabling parts of a module, or of a module as a whole, because they act together in dynamically asserting that a literal, which may be in the body of a rule, is true or false. The recommended practice [7] for designing a set of rules that can be removed from a program being processed in an incremental fashion is to introduce suitable external literals in their bodies. When the external literals are set to true (via \(assign\_external(l)\)), the rules are enabled and used by the solver. When the rules are to be removed from the program, the external literals that control their application are set to false and released by means of \(release\_external(l)\). When that happens, one should also call clingo function \(cleanup()\), which adjusts the internal state of grounder and solver after information has been retracted. _Incremental computations in clingo._ As we mentioned earlier, clingo supports both incremental grounding and incremental solving. Incremental grounding refers to the ability to ground modules in separate stages. When a module is grounded (or an instance of a module, when the module has parameters), it is added to the set of ground rules that clingo maintains. Incremental solving refers to clingo's ability to store and update the state of the search process across multiple solving calls. When a new \(solve()\) call is performed by a programmer, clingo uses the current state of the search process as the starting point of the computation. This approach can potentially yield substantial time savings. As a (trivial) example, consider the case in which one has already grounded and solved a large ASP program and is now interested in adding a new rule. As long as the rule satisfies certain properties, clingo can simply update the truth values of the literals affected by the new rule and avoid repeating the computations linked with the initial program. To make this possible, clingo allows for incremental grounding and solving steps to be interleaved, making it possible for one to ground and solve part of a program, then ground an additional module _with respect to the set of ground literals determined by the previous grounding and solving run_. As a result, the grounding of the new module may be substantially smaller and cheaper to compute than if the initial program and the new module had been grounded in a single operation. _The Module Theorem._ The conditions under which modules can incrementally added to an existing program are given by the Module Theorem [9; 10]. We provide here a summary of this topic adapted from [7]. A _module_\(\mathcal{M}\) is a triple \(\langle P,I,O\rangle\) consisting of a ground logic program \(P\) along with sets \(I\) and \(O\) of ground input and output literals such that:\(I\cap O=\emptyset\),  
\(A(P)\subseteq I\cup O\), and  
\(H(P)\subseteq O\)  
where \(H(P)\) is the set of heads from all rules of \(P\) and \(A(P)=H(P)\cup\bigcup_{r\in P}r^{+}\cup r^{-}\). A set \(X\) of ground literals is an answer set of a module \(\mathcal{P}\) if \(X\) is an answer set of \(P\cup\{a.\mid a\in I\cap X\}\).