On Condensing a Sequence of Updates in Answer-Set Programming

1 Introduction

The growing use of Answer-Set Programming [Gelfond and Lifschitz, 1988; 1991] in dynamic domains calls more and more urgently for plausible and efficient methods for incorporating new, possibly conflicting rules into an answer-set program. Such methods are particularly important when dealing with updates, i.e., when the newly introduced rules represent a change that has occurred in the domain modelled by the program.

Naturally, an update of an answer-set program should result in a new answer-set program that replaces the old one and continues to be used in its place. In other words, the update should be specified as a binary operator on some class of programs over the same alphabet, guaranteeing that updates can be iterated if the need arises. However, despite the large body of work on answer-set program updates, this fundamental requirement has been largely neglected in the literature.

∗Supported by Fundac¸˜ao para a Ciˆencia e a Tecnologia under project "ERRO - Efficient Reasoning with Rules and Ontologies" (PTDC/EIA-CCO/121823/2010).

For instance, the largest group of program update semantics, based on the causal rejection principle [Leite and Pereira, 1998; Alferes et al., 2000; Eiter et al., 2002; Alferes et al., 2005], define stable models for sequences of nondisjunctive programs where each program represents an update of the preceding ones. However, since they sometimes admit non-minimal models, which no non-disjunctive program can capture, they must resort to the introduction of additional meta-level atoms in order to construct a single program whose stable models correspond to the models assigned to the sequence. This leads to difficulties with iterating the update process.

A different approach in [Sakama and Inoue, 2003] deals with program updates by borrowing ideas from literature on belief revision and utilising an abductive framework to accomplish such updates. In this case, multiple alternative programs can be the result of an update and no mechanism is provided to choose among them.

A somewhat similar situation occurs with the approach of [Zhang, 2006] where intricate syntactic transformations are combined with a semantics for prioritised logic programs that ultimately leads to a set of logic programs. Since all of these programs together represent the result of the update, it is once again unclear how to construct a single program that combines all of them.

The rule update semantics suggested in [Delgrande et al., 2007] are also based on syntactic transformations into a logic program with preferences among rules, but in contrast with [Zhang, 2006], the semantics of such programs is defined by directly specifying their preferred stable models and not by translation into an ordinary program (or a set thereof). Thus, although an actual syntactic object is constructed that represents the update, it needs to be interpreted in a richer formalism to take into account preferences among rules.

Finally, frameworks that specify program updates by manipulating dependencies on default assumptions induced by rules [ ˇSefr´anek, 2006; 2011; Kr ¨umpelmann, 2012] are mainly concerned with identifying the effects of irrelevant updates and other theoretical properties of the stable models assigned to a pair or sequence of programs. They do not consider representing the result of an update by a single program.

In this paper, we unravel the true potential of specifying updates as binary operators on some class of programs. Despite the fact that existing program update semantics do not seem compatible with this point of view, we show that at least some of them can be viewed in this manner.

In particular, we return to the foundational approaches to rule updates based on causal rejection, the justified update semantics [Leite and Pereira, 1998], (or JU-semantics for short) as well as the closely related update answer set semantics [Eiter et al., 2002] (or UA-semantics for short). For these, we define binary update operators and show that applying the operator to any sequence of programs produces a program whose stable models coincide with the stable models assigned to the original sequence under JU- and UA-semantics, respectively. In this way, the new operator works as a way to condense any sequence of non-disjunctive programs into a single program that includes all relevant information about the sequence, not only to identify its stable models, but also for the purpose of performing further updates. Thereby, we solve the long-standing problem known as state condensing from the literature on causal rejection semantics for program updates.

To achieve this, our operators must deal with a more general class of programs than non-disjunctive ones. First we define simple and elegant operators that produce nested logic programs [Turner, 2003] with the required property. Subsequently, we show that the full expressivity of nested programs is not necessary for this purpose by defining an additional pair of operators that produce disjunctive logic programs, with default negation in heads of rules to allow for non-minimal stable models, and still maintain the same properties w.r.t. JU- and UA-semantics. Nevertheless, the former operators usually produce more readable programs, sometimes exponentially more concise than the programs returned by the latter ones.

Furthermore, since the update semantics defined in [Alferes et al., 2000; 2005] coincide with JU- and UA-semantics on the class of acyclic programs [Homola, 2004], our results partially extend to those semantics as well.

The remainder of this paper is structured as follows: In Sect. 2 we provide the necessary technical background for our investigation. Section 3 introduces operators for condensing an update sequence into a single nested program while in Sect. 4 we refine the defined operators to work with the more restricted class of disjunctive logic programs. Finally, in Sect. 5 we discuss our findings in a broader context and conclude.

2 Preliminaries

Throughout this paper we consider a fixed finite set of propositional atoms A. We adopt the syntax and stable model semantics of logic programs with nested expressions [Turner, 2003], introduced next. Subsequently, we define the semantics for program updates for which we develop condensing operators in Sects. 3 and 4.

Programs with Nested Expressions

The set of objective literals L consists of all atoms p ∈ A and their (strong) negations ¬p. The opposite literal to an objective literal l is denoted by -l and defined as follows: for any atom p, -p = ¬p and -¬p = p. Elementary formulas are objective literals and the 0-place connectives ⊥ ("false") and ⊤ ("true"). Formulas are built from elementary formulas using the unary connective not (default negation) and the binary connectives ∧ and ∨.

A (nested) rule is an expression π of the form

where h(π) and b(π) are formulas, called the head and body of π. A rule of the form h(π) ← ⊤ is usually identified with the formula h(π). A (nested) program is a finite set of rules.

An interpretation is a consistent set of objective literals. Satisfaction of a formula φ in an interpretation J, denoted by J |= φ, is defined recursively as follows:

• For elementary φ, J |= φ if and only if φ ∈ J or φ = ⊤;
• J |= φ1 ∧ φ2 if and only if J |= φ1 and J |= φ2;
• J |= φ1 ∨ φ2 if and only if J |= φ1 or J |= φ2;
• J |= not φ if and only if J ̸|= φ.

Furthermore, J satisfies a rule π, denoted by J |= π, if J |= b(π) implies J |= h(π), and J satisfies a program P, denoted by J |= P, if J |= π for all π ∈ P.

The reduct of a formula φ relative to J, denoted by φJ , is obtained by replacing, in φ, every maximal occurrence of a formula of the form not ψ with ⊥ if J |= ψ and with ⊤ otherwise. The reducts of a rule π and of a program P are, respectively,

Finally, J is a stable model of a program P if it is subsetminimal among the interpretations that satisfy PJ .

Semantics for Program Updates

Causal rejection semantics for program updates assign stable models to sequences of non-disjunctive programs. Their formal introduction requires a few additional concepts first.

A default literal is a formula of the form not l where l ∈ L. The set of all literals L∗ consists of all objective and default literals. The complementary literal to a literal L is denoted by L and defined as follows: for any objective literal l, l = not l and not l = l.

We say that a rule is disjunctive if its body is either ⊤ or a conjunction of literals and its head is a disjunction of literals; non-disjunctive if its body is either ⊤ or a conjunction of literals and its head is a literal. A program is disjunctive if all its rules are disjunctive; non-disjunctive if all its rules are non-disjunctive.

Now we can proceed with defining the JU-semantics [Leite and Pereira, 1998] and UA-semantics [Eiter et al., 2002] for program updates. Both semantics can be seen as formal embodiments of the causal rejection principle which states that every rule must remain in effect as long as it is not contradicted by a newer rule. We define them in their generalised forms, allowing for default negation in heads of rules [Leite, 2003]. 1

A dynamic logic program (DLP) is a finite sequence of non-disjunctive programs. Given a DLP P, we denote by all(P) the set of all rules belonging to the programs in P . 2

A conflict between rules occurs when the head literal of one rule is the default or strong negation of the head literal of the other rule. Similarly as in [Leite, 2003], we consider the conflicts between an objective literal and its default negation as primary while conflicts between objective literals are translated into a primary conflict by expanding the DLP accordingly. This expansion employs the coherence principle: when an objective literal l is derived, its complement -l cannot be concurrently true and thus not -l must be true. Formally, for a DLP P = 〈Pi〉i<n, the expanded version of P is the DLP P ∗ = 〈P∗i 〉i<n where for every i < n,

Furthermore, we say that rules π, σ are in conflict, denoted by π ✶ σ, if h(π) = h(σ).

The JU-semantics [Leite and Pereira, 1998] defines a set of rejected rules, which depends on a stable model candidate, and then verifies that the candidate is indeed a stable model of the remaining rules.

Definition 1 (JU-Semantics [Leite and Pereira, 1998]). Let P = 〈Pi〉i<n be a DLP and J an interpretation. The set of rejected rules rej JU (P, J) contains all rules π ∈ Pi such that for some rule σ ∈ Pj with j > i,

The set [[P ]]JU of JU-models of a DLP P consists of all interpretations J such that J is a stable model of the program

Under the JU-semantics, a rule π is rejected if a more recent rule σ is in conflict with π and the body of σ is satisfied in the stable model candidate J. The only difference in the UA-semantics [Eiter et al., 2002] is that rejected rules are prevented from rejecting other rules:

Definition 2 (UA-Semantics [Eiter et al., 2002]). Let P = 〈Pi〉i<n be a DLP and J an interpretation. The set of rejected rules rej UA (P , J) contains all rules π ∈ Pi such that for some rule σ ∈ Pj with j > i,

1 Default negation in heads of rules enhances the expressivity of the formalism as it allows us to express that an objective literal should cease being true, distinguishing this case from the one where the opposite literal must become true.

2 In order to avoid issues with rules that are repeated in multiple components of a DLP, we assume throughout this paper that every rule is uniquely identified in all set-theoretic operations. This can be formalised by assigning a unique name to each rule and performing operations on names instead of the rules themselves. However, for the sake of simplicity, we leave the technical realisation to the reader.

3 Note that although this definition is recursive, the defined set is unique. This is because we assume that every rule is uniquely identified and to determine whether a rule fromPi is rejected, the recursion only refers to rejected rules from programs Pj with j strictly greater than i. One can thus first find the rejected rules in Pn-1 (always ∅ by the definition), then those in Pn-2 and so on until P0.

The set [[P ]]UA of UA-models of a DLP P consists of all interpretations J such that J is a stable model of the program

The main difference between these semantics is that the latter is more sensitive to irrelevant updates, such as an update by a tautological rule that cannot indicate any change in the modelled world because it is always satisfied. One example that distinguishes the JU- and UA-semantics is the DLP

for which the only JU-model is { ¬p }, while, due to the presence of the last rule, the UA-semantics admits the additional undesired model { p }.

3 Condensing into a Nested Program

Now that all technical preliminaries are covered, we can proceed with the definition of a state condensing operator for the JU-semantics, and subsequently also for the UA-semantics. More specifically, we will define binary operators ⊕JU and ⊕UA that take an original program and its update as arguments and return the updated program. We naturally generalise any such operator ⊕ to a sequence of programs P = 〈Pi〉i<n inductively as follows:⊕〈〉 = ∅ ,

The property that ⊕JU and ⊕UA must fulfill is that for any DLP P, the stable models of the program ⊕JU P are exactly the JU-models of P and, similarly, the stable models of the program ⊕UA P are exactly the UA-models of P .

Both ⊕JU and ⊕UA are defined by utilising the concept of an activation formula, which captures the condition under which literal L is derived by some rule in a program U. Formally, the activation formula for L in U is defined as follows:

The operator ⊕JU is based on the following simple idea: When updating a program P by a program U, each rule π from P∗ with literal L in its head must be disabled when some rule from U ∗ for the literal complementary to L is activated. This can be achieved by augmenting the body of π with the additional condition not αU ∗(L). Formally:

Definition 3 (Condensing operator ⊕JU). A JU-rule is a rule with a single literal in its head and a JU-program is any set of JU-rules.

The binary operator ⊕JU on the set of all JU-programs is defined as follows: Given two JU-programs P and U, the JU-program P ⊕JU U consists of the following rules:

1. for all π ∈ P∗ , the rule

2. all rules in U ∗ .

p ← not ((not q ∧ not r) ∨ s) not ¬p q ← p not ¬q ← p r ← not ⊤ not ¬r not p ← not q ∧ not r ∧ not s not p ← s ∧ not s not r ← not r p ← s not ¬p ← s s r ← r not ¬r ← r not ¬s

The following example illustrates the relationship between the JU-semantics and the condensing operator ⊕JU, while the subsequent theorem pinpoints the fact that it actually holds in general.

Example 4. Suppose that programs P, U are as follows:

In addition to the rules from U ∗ (which in this case coincides with U), the program ⊕JU 〈P, U〉 contains the following six rules: 5

Also, the two stable models of ⊕JU 〈P, U〉 are ∅ and { p, q }, and they coincide with the JU-models of the DLP 〈P, U〉.

Now consider that V contains the following three rules:

The program ⊕JU 〈P, U, V〉 contains the following rules:

• the six rules listed in (2);
• the following rules, which originate in U:

• all rules in V ∗ .

The full program is also shown in Fig. 1. Its unique stable model is {p, q, s}, which coincides with the unique JU-model of 〈P, U, V〉.

Theorem 5 (State condensing using ⊕JU). Let P be a DLP. An interpretation J is a JU-model of P if and only if it is a stable model of ⊕JU P .

Thus, the single nested program P = ⊕JU P faithfully represents P in the sense that it captures all information from P that is relevant w.r.t. the JU-semantics: not only does it have the required stable models, but any further updates of P can be performed directly on P by applying the operator ⊕JU and the obtained stable models will be the same.

4 Note that ∨ ∅ is simply ⊥.

5 For the sake of readability, we omit the conjuncts ⊤ and not ⊥ in rule bodies.

p ∨ not q ← not s not ¬p p ∨ not r ← not s not ¬q ← p q ← p not ¬r not p ← not q ∧ not r ∧ not s not p ← s ∧ not s not r ← not r p ← s not ¬p ← s s r ← r not ¬r ← r not ¬s

In case of the UA-semantics, a very similar operator can be used to obtain the same result. The only difference is that for a DLP P = 〈Pi〉i<n, in addition to the rules in ⊕JU P, the program ⊕UA P will also contain the choice rule

for all i < n and every rule π ∈ Pi with h(π) ∈ L. Intuitively, these additional rules account for the differences in the definition of rej JU (P , J) and rej UA (P , J). They make sure that no rule is ever completely eliminated due to extra conditions added to its body, but stays partially in effect by generating alternative worlds for the objective literal in its head: one where it is satisfied and one where it is not. Essentially, this means that whenever the original body of the rule is satisfied, its head cannot be assumed false by default.

Definition 6 (Condensing operator ⊕UA). A UA-rule is a rule with either a single literal or a disjunction of two literals L and L in its head, and a UA-program is any set of UA-rules.

The binary operator ⊕UA on the set of all UA-programs is defined as follows: Given two UA-programs P and U, the UA-program P ⊕UA U consists of the following rules:

1. for all π ∈ P∗ with h(π) ∈ L∗ , the rule

1. all π ∈ P such that h(π) is of the formL∨L;
2. for all π ∈ U with h(π) ∈ L, the rule

4. all rules in U ∗ .

Similarly as with the operator ⊕JU, we first illustrate the inner workings of operator ⊕UA on an example, highlighting its difference from ⊕JU as well as its relationship with the UA-semantics, and then formally establish this relationship in the general case.

Example 7. Consider again the programs P, U and V from Example 4. Except for the rules in ⊕JU 〈P, U〉, the program ⊕UA 〈P, U〉 also contains the following three rules:

Nevertheless, its stable models, ∅ and { p, q }, are the same as those of ⊕JU 〈P, U〉, and they also coincide with the UA-models of the DLP 〈P, U〉.

p ← not ((not q ∧ not r) ∨ s) not ¬p q ← p not ¬q ← p r ← not ⊤ not ¬r p ∨ not p q ∨ not q ← p r ∨ not r not p ← not q ∧ not r ∧ not s not p ← s ∧ not s not r ← not r p ← s not ¬p ← s s r ← r not ¬r ← r not ¬s p ∨ not p ← s r ∨ not r ← r s ∨ not s

The situation is more interesting after V is added to the sequence. The resulting program ⊕UA 〈P, U, V〉 contains all the rules in ⊕JU 〈P, U, V〉, the three rules listed in (3) and, additionally, the following three rules:

For reference, the entire program is also listed in Fig. 3. Due to the last rule in (3), it has the extra stable model { p, q, r, s } in addition to the unique stable model { p, q, s } of ⊕JU 〈P, U, V〉. These stable models also coincide with the UA-models of the DLP 〈P, U, V〉.

Theorem 8 (State condensing using ⊕UA). Let P be a DLP. An interpretation J is a UA-model of P if and only if it is a stable model of ⊕UA P .

As with the JU-semantics, the significance of this theorem is in that the operator ⊕UA provides a full characterisation of the UA-semantics: It can condense any given DLP P into a single nested program P such that the stable models of P coincide with the UA-models of P and any further updates on top of P can be equivalently performed on P using ⊕UA.

4 Condensing into a Disjunctive Program

The condensing operators defined in the previous section can be further modified in order to produce a program that meets certain additional requirements. In the present section we show that nested expressions can be completely eliminated from the resulting program while still preserving the same tight relationship with the original program update semantics. Thus, we introduce a new pair of operators, ⊕∨JU and ⊕∨UA, that operate on disjunctive programs with default negation in heads of rules. Note that due to the non-minimality of JU- and UA-models for certain DLPs, disjunctive programs without default negation in heads of rules would already be insufficient for this purpose.

The ideas underlying the new operators are fairly straightforward. Essentially, nested expressions are introduced into the resulting programs only by the negations of activation formulas in their bodies, so these are the parts of rules that need to be translated into conjunctions in bodies and disjunctions in heads of rules. In particular, by utilising De Morgan's law and distributivity of conjunction over disjunction, we can obtain a new formula, a disjunction of conjunctions of default literals and double-negated objective literals, that is strongly

Figure 4: The program ⊕∨UA 〈P, U, V〉

equivalent to the original formula. For instance, in case of the first rule in (2), we can equivalently write the condition not((not q ∧ not r) ∨ s) as

Then it suffices to break up the resulting rule into multiple rules, each with one of the disjuncts of this formula in the body, and remove one of the negations from each doublenegated literals and "move" it into the head of the newly constructed rule. In case of the first rule in (2), the result would be the following two disjunctive rules:

Formally, we call the set of literals, without double negation, within each of the disjuncts described above a blocking set. Given a non-disjunctive program U and a literal L, if the formula αU(L) contains ⊤ as one of its disjuncts, then there is no blocking set for L in U. Otherwise, suppose that αU(L) is the formula

A blocking set for L in U is any set of literals

where 1 ≤ ij ≤ kj for every j with 1 ≤ j ≤ n. We denote the set of all blocking sets for L in U by βU(L). Also, for any set of literals S,

Each nested rule

can thus be replaced by a set of disjunctive rules

where S ∈ βU ∗ (h(π)). Furthermore, when h(π) is a default literal, it is more convenient to move the new default literals from the head into the body since this operation preserves stable models [Inoue and Sakama, 1998] and makes it easier to pinpoint the original head literal in the rule. This leads us to the following definition of ⊕∨JU:

Definition 9 (Condensing operator ⊕∨JU). The binary operator ⊕∨JU on the set of all disjunctive programs is defined as follows: Given two disjunctive programs P and U, the disjunctive program P ⊕∨JU U consists of the following rules:

1. for all π ∈ P∗ such that for some l ∈ L, either h(π) = l or l is the unique non-negated disjunct of h(π), and all S ∈ βU ∗(not l), the rule

1. for all π ∈ P∗ such that for some l ∈ L, h(π) = not l, and all S ∈ βU ∗(l), the rule

3. all rules in U ∗ .

If we consider the programs P, U and V from Example 4, the disjunctive program ⊕∨JU 〈P, U, V〉 differs from the nested one in two points: 1) its only nested rule is turned into the two disjunctive rules in (4), and 2) the rule r ← not ⊤ is completely eliminated because its body is never satisfied and, formally, there is no blocking set for not r in U. For comparison, Fig. 2 includes a listing of the rules in ⊕∨JU 〈P, U, V〉.

The operator ⊕∨JU preserves the main property of ⊕JU.

Theorem 10 (State condensing using ⊕∨JU). Let P be a DLP. An interpretation J is a JU-model of P if and only if it is a stable model of ⊕∨JU P .

As for the UA-semantics, analogical modifications can be applied in the definition of ⊕UA to obtain an operator that produces a disjunctive program. Furthermore, due to the additional choice rules included in the result, the rules can be further simplified, when compared to the rules produced by ⊕∨JU. In particular, the first group of rules can be treated the same way as the second, leading to the following definition of ⊕∨UA:

Definition 11 (Condensing operator ⊕∨UA). The binary operator ⊕∨UA on the set of all disjunctive programs is defined as follows: Given two disjunctive programs P and U, the disjunctive program P ⊕∨UA U consists of the following rules:

1. for all π ∈ P∗ with h(π) ∈ L∗ and all S ∈ βU ∗ (h(π)), the rule

1. all π ∈ P such that h(π) is of the formL∨L;
2. for all π ∈ U with h(π) ∈ L, the rule

4. all rules in U ∗ .

Returning to the programs P, U and V from Example 4, the differences between programs ⊕∨UA 〈P, U, V〉 and ⊕UA 〈P, U, V〉 are similar to those between ⊕∨JU 〈P, U, V〉 and ⊕JU 〈P, U, V〉 and the rules of ⊕∨UA 〈P, U, V〉 are listed in Fig. 4. Also, ⊕∨UA preserves the main property of ⊕UA.

Theorem 12 (State condensing using ⊕∨UA). Let P be a DLP. An interpretation J is a UA-model of P if and only if it is a stable model of ⊕∨UA P .

Although operators ⊕∨JU and ⊕∨UA eliminate the necessity for using nested rules to condense a DLP into a single program, this comes at a cost. Namely, the size of the nested program resulting from applying operators ⊕JU and ⊕UA is always linear in size of the argument programs, while in case of ⊕∨JU and ⊕∨UA, the resulting program can be exponentially larger. Furthermore, Figs. 1 to 4 suggest that the representations produced by ⊕∨JU and ⊕∨UA will be less faithful to the form of the rules in the original programs, and thus less readable. This indicates that the nested program is more suitable as a way to store the condensed program, both in terms of space and readability. Additionally, in order to find its stable models, a more efficient translation can be used that utilises additional atoms to prevent the exponential explosion. However, such a translation will no longer be equivalent to the original program sequence w.r.t. performing further updates.

5 Discussion

Defining update operators for answer-set programs that actually produce an answer-set program written in the same alphabet has been a long enduring problem, also known as state condensing, i.e., condensing a sequence of answer-set programs - interpreted as updates - into a single answer set program. Existing semantics typically proceed by characterising the models of the update and, at most, either describe a set of answer-set programs that could represent the update, instead of only one, or produce an answer-set program written in a language extended with a considerable amount of new atoms, making it difficult to understand and to further update.

Part of the problems emerge because some semantics employ complex mechanisms such as preferences or other minimality criteria that make it impossible to encode the result in a single answer-set program, while others have model-theoretic characterisations that assign non-minimal models to certain update sequences, and it is well known that stable models of non-disjunctive answer-set programs are minimal.

In this paper we addressed and solved the problem of state condensing for two of the most relevant semantics for updates, by resorting to more expressive classes of answer-set programs, namely nested and disjunctive. In all four cases, two for each semantics using both classes of answer-set programs, the resulting program is written with the same alphabet and is ready to be further updated. We have illustrated with some examples that the resulting programs written using nested answer-set programming are perhaps more readable than those written using disjunctive answer-set programs, in the sense that they more closely match the intuitions underlying the semantics for updates that we consider.

A similar approach to answer-set program updates has previously been considered by Osorio and Cuevas [2007] but the possibility of performing iterated updates has not been explored. This work is also related to our work on semantic rule updates [Slota and Leite, 2010; 2012a] where state condensing is taken as one of the basic characteristics of rule updates, making it possible to relate them more directly with classical belief update principles and semantics [Slota and Leite, 2012b]. In the future, it would also be interesting to look for condensing operators for other rule update semantics.