Forgetting Auxiliary Atoms in Forks (Extended Abstract)

1 Introduction

Answer Set Programming (ASP [Baral, 2003]) has become an established problem-solving paradigm for Knowledge Representation and Reasoning (KRR). The reasons for this success derive from the practical point of view, with the availability of efficient solvers [Gebser et al., 2012; Faber et al., 2008] and application domains [Erdem et al., 2016], but also from its solid theoretical foundations, rooted in the stable models [Gelfond and Lifschitz, 1988] semantics for normal logic programs that was later generalised to arbitrary propositional [Pearce, 1996], first-order [Pearce, 2006; Ferraris et al., 2007] and infinitary [Harrison et al., 2015] formulas. An important breakthrough that supported these extensions of ASP has been its logical characterisation in terms of Equilibrium Logic [Pearce, 1996] and its monotonic basis, the intermediate logic of Here-and-There (HT). Despite its expressiveness, a recent result [Gonc¸alves et al., 2016] has shown that Equilibrium Logic has limitations in capturing the representational power of auxiliary atoms, which cannot always be forgotten.

∗This paper is an extended abstract of an article entitled Forgetting Auxiliary Atoms in Forks and published in Artificial Intelligence [Aguado et al., 2019].

In this paper, we extend logic programs to include a new construct ' | ' we call fork and whose intuitive meaning is that the stable models of P | P ′ correspond to the union of stable models from P and P ′ in any context. We also review the notion of projective strong equivalence (PSE), that is, whether two programs are equivalent over a restricted vocabulary in any context that uses also the same restricted vocabulary [Eiter et al., 2005]. Finally, we show that using this construct is always possible to forget any set of atoms, something that was not possible without it.

2 Motivation Example

To illustrate this point, take the following problem.

Example 1 Two individuals, mother and father, both carrying alleles a and b, procreate an offspring. We want to generate all the possible ways in which the offspring may inherit its parents' genetic information.

According to Mendelian laws, we should obtain three possible combinations that, ignoring their frequency, correspond to the sets of alleles {a}, {b} and {a, b}. These are, in fact, the three classical models of disjunction a∨b. To obtain these three solutions as stable models in ASP, the straightforward way would be to use the three rules:

We assume here some familiarity with ASP: disjunctions of the form p ∨ ¬p act as non-deterministic choice rules (allowing the arbitrary inclusion of atom p) and ⊥←¬a ∧¬b is a constraint forbidding models where a ∨ b does not hold. Moreover, when we include p∨¬p for all atoms, as in the example, stable models just coincide with classical models. A drawback of this representation is that it does not differentiate the information coming from each parent, possibly becoming a problem of elaboration tolerance. For instance, if only the mother's information were available, one would expect to obtain the stable models {a} and {b} but not {a, b}, as there is no evidence of that combination without further information about the father. So, the mother alone would be better represented by a regular disjunction a ∨ b. However, we cannot represent each parent as an independent disjunction like that, since (a ∨ b) ∧ (a ∨ b) just amounts to (a ∨ b) and the combination {a, b} is not obtained. A simple way to represent these two disjunctions separately is using auxiliary atoms to keep track of alleles from the mother (ma ∨ mb) and the father (fa ∨ fb). This leads to program P2:

consisting of the mother's contribution Pm and the father's contribution Pf . Four stable models are obtained from P2, {ma, fa, a}, {mb, fb, b}, {ma, fb, a, b} and {mb, fa, a, b}, but if we project them on the original vocabulary V = {a, b} (i.e. we remove auxiliary atoms), they collapse to three {a}, {b} and {a, b} as expected. Note that, although auxiliary atoms in this example have a meaning in the real world (they represent the effective sources of each inherited allele) they were not part of the original alphabet V = {a, b} of Example 1, which does not distinguish between the same effect {a, b} but due to different sources {ma, fb, a, b} and {mb, fa, a, b}.

As we have seen, P1 and P2 are "V -equivalent" in the sense that they yield the same stable models when projected to alphabet V = {a, b}. A natural question is whether this also holds in any context, that is, if P1 ∪Q and P2 ∪Q also yield the same V -projected stable models, for any context Q in the target alphabet V (since we want to keep auxiliary atoms local or hidden). As mentioned before, we call this notion projective strong equivalence w.r.t. V , or V -strong equivalence for short.

As we will see later, programs P1 and P2 are indeed V -strongly equivalent, so they express the same combined knowledge obtained from both parents. However, if we want to keep program Pm alone capturing the mother's contribution, there is no possible {a, b}-strongly equivalent representation in Equilibrium Logic (the same happens with Pf ).

3 Forks and T-views

Let At be a finite set of atoms called the (propositional) signature. A (propositional) formula ϕ is defined using the grammar:

where p is an atom p ∈ At. We use Greek letters ϕ, ψ, γ and their variants to stand for formulas. A fork is defined using the grammar:

where ϕ is a propositional formula and p ∈ At is an atom. We use Greek letters F,G,H and their variants to stand for forks. We define the derived operators ¬ϕ def = (ϕ→⊥) and ⊤ def = ¬⊥. Notice that the fork operator '|' cannot occur in the scope of disjunction or negation, since ¬F would stand for F → ⊥ and implications do not allow forks in the antecedent. This restricted syntax suffices for the purposes of the current paper.

The semantics of forks is defined in terms of denotations in two steps. First we define the denotation of propositional formulas and then we extend it to arbitrary forks.

Given a set T of atoms, a T-support H is a set of subsets of T, that is H ⊆ 2T , satisfying T ∈ H if H ̸= ∅. We write HT to stand for the set of all possible T-supports. To increase readability of examples, we just write a support as a sequence of interpretations between square brackets. For instance, possible supports for T = {a, b} are [{a, b} {a}], [{a, b} {b} ∅] or the empty support [ ].

Intuitively, H will be used to capture the set of "here" components H that support the "there" world T as a model of a given formula ϕ, that is, the set of H's such that 〈H, T〉 |= ϕ in here-and-there logic. When H is empty [ ], there is no support for T, so 〈T, T〉 ̸|= ϕ and thus, T is not even a classical model. If H is not empty, this means we have at least some model 〈H, T〉 and, thus, 〈T, T〉 must be a model too; this is why we require T ∈ H in the set.

Definition 1 (T-denotation; Aguado et al. 2015) Let T ⊆ At. The T-denotation of a formula ϕ, written JϕKT , is a T-support recursively defined as follows:

T-denotations satisfy that H ∈ JϕKT iff 〈H, T〉 |= ϕ in the logic of here-and-there. Interestingly, when not empty, the fewer models in JϕKT , the more supported is T, since it is closer to being stable. Seeing "more supported" as an ordering relation, the "most supported" JϕKT (the top element) would precisely be JϕKT = [ T ] corresponding to a stable model. This ordering relation is formally defined below.

Definition 2 Given a set T ⊆ At of atoms and two Tsupports H and H′ we write H ⪯T H′ iff either H = [ ] or H ⊇H′ ̸= [ ].

The relation ⪯T is a partial order onHT with [ ] and [ T ] its bottom and top elements, respectively. We usually write H ⪯ H′ instead of H ⪯T H′ when clear from the context. As an example, the classical interpretation T = {a, b} is more supported in H1 = [{a, b} {a}] than in H2 = [{a, b} {a} {b} ∅], that is H2 ⪯ H1, because H2 contains additional interpretations and is further from being stable.

Example 2 (Implementing a choice) To implement a choice rule for atom p (in modern ASP syntax, written {p}) a knowledge engineer uses an auxiliary atom q. As a first option, she considers the use of rules:

However, having a disjunctive ASP solver, another possibility could be:

Is there any substantial difference?

□

The T-denotations of both options are shown in Figure 1. As mentioned above, stable models correspond to T's such that JϕKT = [ T ], that is, we get the two stable models {p} and {q} in both columns. In fact, all rows coincide except for T = {p, q} where ∅ ∈ J (1) K{p,q} but ∅ ̸∈ J (2) K{p,q} . A difference in T-denotations means that formulas are not HT equivalent, and so, they are not strongly equivalent [Lifschitz et al., 2001]. In fact, the counterexample of strong equivalence is well-known in the literature: adding (p → q) ∧ (q → p) to (1) yields no stable model, while the same addition to (2) produces stable model {p, q}.

Let us now introduce the semantics of arbitrary forks. Given a T-support H we define the set of (non-empty) ⪯- smaller supports ↓H = {H′ | H′ ⪯ H} \ { [ ] }. This is usually called the ideal of H. Note that, the empty support [ ] is not included in the ideal. As a result, ↓[ ] = ∅. We extend this notation to any set of supports ∆ so that ↓∆ def = { H′ ∣∣ H′ ⪯H,H ∈ ∆ } \ { [ ] }.

Definition 3 (T-view) A T-view is a set of T-supports ∆ ⊆ HT that is ⪯-closed, i.e., ↓∆=∆.

If ∆ is a T-view and the ⪯-greatest T-support [ T ] is included in ∆, then ∆ is precisely ↓[ T ]. We proceed next to define the semantics of forks in terms of T -views. To emphasize the duality between conjunction and disjunction, we will be interested in dealing with a weaker version of the membership relation, ˆ∈, defined as follows. Given a T-view ∆, we write H ˆ∈ ∆ iff H ∈ ∆ or both H = [ ] and ∆ = ∅. We are now ready to extend the concept of T -denotation to forks.

Definition 4 (T-denotation of a fork) Let At be a propositional signature and T ⊆ At a set of atoms. The T -denotation of a fork F, written 〈〈F 〉〉T , is a T-view recursively defined as follows:

The fork operator '|' is commutative, associative and idempotent. Conjunction and implication distribute over '|'. As for the rest of operators, note that the definitions above also cover propositional formulas. In fact, we have the following relation between T-denotations as T-views and T-supports: 〈〈ϕ〉〉T =↓JϕKT for every propositional formula ϕ.

Definition 5 Given a fork F , we say that T ⊆ At is a stable model of F iff 〈〈F 〉〉T = ↓[ T ]. SM[F] denotes the set of stable models of F .

For any propositional formula, this definition coincides with the standard definition of stable models. The intuition behind a fork is that we can collect its stable models independently, that is, SM[F | G] = SM[F] ∪ SM[G].

4 Projective Strong Equivalence

Let us now formally define projective strong equivalence for forks. Since propositional formulas are also forks, this definition also applies to them. We represent the projection of the stable models of some fork onto some vocabulary V as SMV [ϕ] def = {T ∩ V | T ∈ SM[ϕ] }.

Definition 6 (Projective strong equivalence) Let V ⊆ At be some vocabulary. A fork F is V -strongly equivalent to fork G, written F ∼=V G if SMV [F ∧L] = SMV [G∧L] for any fork L such that At(L) ⊆ V .

When V ⊇ At(F) ∪At(G) we talk about (non-projective) strong equivalence and drop the V subindex. Strong equivalence has a simple characterisation in these terms: F ∼= G iff 〈〈F 〉〉T = 〈〈G〉〉T for every T ⊆ At.

Providing a semantic characterisation of projective strong equivalence ∼=V requires some more notation. We define HV as the projection of every set in H to the vocabulary V , i.e., HV def = {H∩V | H ∈ H}. A T -support H is V -unfeasible iff there is some H ⊂ T in H satisfying H ∩ V = T ∩ V ; it is V -feasible otherwise. The reason for the name "unfeasible" is that, if we take a formula ϕ with denotation JϕKT = H, then T will never become stable if we are only allowed to use vocabulary V when adding a context γ.

Definition 7 Let V ⊆ At be a vocabulary and T ⊆ V be a set of atoms. Then, the V -T-denotation of a fork F is a T-view, denoted as 〈〈F 〉〉TV , is defined as follows:

In other words, 〈〈F 〉〉TV collects all the feasible supports H that belong to any T ′ -denotation 〈〈F 〉〉T ′ such that T ′ coincides with T for atoms in V , and then we project the supports taking HV . In doing so, we can just consider maximal H's in 〈〈F 〉〉T ′ . As might be expected, projecting the T-denotation of a fork F on a superset V ⊇ At(F) of its atoms produces no effect, that is, 〈〈F 〉〉TV = 〈〈F 〉〉T . More interestingly, the V -T -denotation of F can be used to precisely characterise its projected stable models and projective strong equivalence.

Theorem 1 For any vocabulary V ⊆ At, set of atoms T ⊆ V and forks F,G, the following holds:

• (i) T ∈ SMV [F] iff 〈〈F 〉〉TV = ↓[ T ].
• (ii) F ∼=V G iff 〈〈F 〉〉TV = 〈〈G〉〉TV for every set T ⊆ V of atoms.

Example 3 (Ex. 2 continued) We can now check the PSE of (1) = (¬p → q) ∧ (¬q → p) and (2) = (p ∨ q). To do so, we have to test if 〈〈 (1) 〉〉TV = 〈〈 (2) 〉〉TV for every T ⊆ V and any vocabulary V not containing q. Since J (1) KT = J (2) KT for all but T = {p, q} we can restrict ourselves to the study to At = {p, q} and V = {p}. Take 〈〈 (1) 〉〉TV first. Since (1) is a propositional formula (it contains no forks), we have 〈〈 (1) 〉〉T ′ =↓ J (1) KT ′ , that is, the maximal supports are just the T-denotations we already obtained in Figure 1. Now, for vocabulary V = {p} we may only have T = {p} and T = ∅. For the first case, the potential candidates T ′ such that T ′ ∩ V = {p} are the rows T ′ = {p} and T ′ = {p, q} from Figure 1. However, the support we have for the latter is V -unfeasible because it contains H = {p} with H ⊂ {p, q} = T ′ and H ∩ V {p} = T ′ ∩ V . Thus, for T = {p} we only have the feasible (maximum) support [{p}] from T ′ = {p} which yields 〈〈 (1) 〉〉TV =↓[ {p} ]. For T = ∅ the only non-empty case is T ′ = {q} and, after removing atom q, we obtain [∅] as maximum support, i.e., 〈〈 (1) 〉〉∅V = ↓[ ∅ ]. It is easy to see that (2) yields the same result: the only difference we have is in the last row of Figure 1, for T ′ = {p, q}, but this support is V -unfeasible again, as it also contains H = {p}. To sum up 〈〈 (1) 〉〉TV = 〈〈 (2) 〉〉TV =↓[ {p} ] and 〈〈 (1) 〉〉∅V = 〈〈 (2) 〉〉∅V =↓ [ ∅ ] so both formulas satisfy PSE, that is, (1) ∼=V (2).

5 Forgetting

We show now how the addition of forks allows us to define a strong persistent forgetting operator that is applicable to any fork and, thus, to any formula. As mentioned in the introduction, this is not possible without the fork operator. Formally, given a T-support H, we denote by ΦH a propositional formula such that JΦH KT =H. Such a formula always exists and the process to build it was studied by Cabalar and Ferraris [2007].

Definition 8 (Forgetting operator) The fork-forgetting operator fk is a function mapping forks and sets of atoms to forks such that

Operator fk is a total, strongly persistent forgetting operator over forks. This is formalised as follows.

Example 4 (Ex. 1 continued) Consider program Pm from the introduction interpreted as the conjunction of its rules, and assume we want to forget ma and mb. The table in Figure 2 shows the T-V -denotation of Pm for each T ⊆ V = {a, b}. Cases for T = {a} and T = {b} are easy to compute. For T = {a, b} we get three candidate interpretations, T ′1 = {ma, a, b}, T ′2 = {mb, a, b} and T ′3 = {ma,mb, a, b}. The table in Figure 3 shows the T-views of Pm for these T ′ i . A first observation is that the support for T ′3 = {ma, mb, a, b} is {a, b}-unfeasible because it contains {ma, a, b} and {mb, a, b} that coincide with T ′3 for atoms {a, b}. After removing ma,mb in the supports of the feasible candidates, T ′1 and T ′2 , the respective results are [ {a, b} {a} ] and [ {a, b} {b} ] that are not ⪯-comparable. Therefore, they become the two ⪯-maximal supports in the last row of Figure 2. It is also easy to check that the T-denotations of fork a | b exactly coincide with the one shown in Figure 2 for Pm. Therefore, Pm ∼=V (a | b). It also can be checked that, after some simplifications, the forgetting operator, fk(Pm, V ), precisely produces the fork (a | b).

6 Conclusions

We extended the syntax and semantics of Here-and-There (HT) to deal with a new type of construct '|' called fork. We studied the property of projective strong equivalence (PSE) for forks: two forks satisfy PSE for a vocabulary V iff they yield the same stable models projected on V for any context over V . We also provided a semantic characterisation of PSE that allowed us to prove that it is always possible to forget (under strong persistence) an auxiliary atom in a fork, something recently proved to be false in standard HT.

Acknowledgements

This work was partially supported by MINECO (TIN201784453-P), Xunta de Galicia (GPC ED431B 2019/03) and the Salvador de Madariaga programme, Spain; by the European Regional Development Fund (ERDF). The third author is supported by the Alexander von Humboldt Foundation.