In this work we tackle the problem of checking strong equivalence of logic programs that may contain local auxiliary atoms, to be removed from their stable models and to be forbidden in any external context. We call this property projective strong equivalence (PSE). It has been recently proved that not any logic program containing auxiliary atoms can be reformulated, under PSE, as another logic program or formula without them - this is known as strongly persistent forgetting. In this paper, we introduce a conservative extension of Equilibrium Logic and its monotonic basis, the logic of Here-and-There, in which we deal with a new connective '|' we call fork. We provide a semantic characterisation of PSE for forks and use it to show that, in this extension, it is always possible to forget auxiliary atoms under strong persistence. We further define when the obtained fork is representable as a regular formula.
Answer Set Programming (ASP [
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}. The straightforward way to generate these three stable models is to encode an inclusive disjunction with the following 3 rules: a ∨ ¬a b ∨ ¬b ⊥ ← ¬a ∧ ¬b (P1) 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 (f a ∨ f b). This leads to program P2: ma ∨ mb f a ∨ f b a ← ma a ← f a b ← mb b ← f b (Pm) (Pf ) consisting of the mother’s contribution Pm and the father’s contribution Pf . Four stable models are obtained from P2, {ma, f a, a}, {mb, f b, b}, {ma, f b, a, b} and {mb, f a, 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, f b, a, b} and {mb, f a, 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). This is obviously a kind
of strong equivalence relation [
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 ). In other words, we cannot forget atoms ma and
mb in Pm and get a program preserving PSE. This impossibility follows from a
recent result in [
In this paper, we extend logic programs to include a new construct ‘ | ’ we call fork whose intuitive meaning is that the stable models of P | P 0 correspond to the union of stable models from P and P 0 in any context2 Q, that is SM [(P | P 0) ∧ Q] = SM [P ∧ Q] ∪ SM [P 0 ∧ Q]. Using this construct, we can represent Example 1 as the conjunction of two forks (a | b) ∧ (a | b), one per each parent. This conjunction of forks is not idempotent but will actually amount to (a | b | a ∧ b). We will show that forgetting is always possible in forks but some of them, such as (a | b), cannot be represented in Equilibrium Logic unless we allow the introduction of auxiliary atoms.
The rest of the paper is organised as follows. Section 2 recalls basic definitions of HT and Equilibrium Logic. Section 3 introduces an alternative characterisation of HT in terms of T -supports. The next section extends the syntax with the fork connective and generalises the semantics to sets of T -supports (so-called T -views). In Section 5 we characterise PSE for forks and relate this property to forgetting. Finally, Section 6 discusses related work and concludes the paper. 2
We begin by recalling some basic definitions and results related to HT. Let At be a set of atoms called the propositional signature. A (propositional) formula ϕ is defined using the grammar: ϕ ::= ⊥ p ϕ ∧ ϕ ϕ ∨ ϕ ϕ → ϕ 1 It corresponds to relativised strong equivalence (with respect to V ) with projection (with respect to V ). 2 For simplicity, we understand programs as the conjunction of their rules. where p is an atom. We will use Greek letters ϕ, ψ, γ and their variants to stand for formulas. We define the derived operators ¬ϕ d=ef (ϕ → ⊥) and > d=ef ¬⊥ and ϕ ↔ ψ d=ef (ϕ → ψ) ∧ (ψ → ϕ). Given a formula ϕ, by At(ϕ) ⊆ At we denote the set of atoms occurring in ϕ. For simplicity, we consider finite theories understood as the conjunction of their formulas. The extension to infinite theories is straightforward.
A classical interpretation T is a set of atoms T ⊆ At. We write T |= ϕ to stand for the usual classical satisfaction of a formula ϕ. An HT-interpretation is a pair hH, T i (respectively called “here” and “there”) of sets of atoms H ⊆ T ⊆ At; it is said to be total when H = T . The fact that an interpretation hH, T i satisfies a formula ϕ, written hH, T i |= ϕ, is recursively defined as follows: – hH, T i 6|= ⊥ – hH, T i |= p iff p ∈ H – hH, T i |= ϕ ∧ ψ iff hH, T i |= ϕ and hH, T i |= ψ – hH, T i |= ϕ ∨ ψ iff hH, T i |= ϕ or hH, T i |= ψ – hH, T i |= ϕ → ψ iff both (i) T |= ϕ → ψ and (ii) hH, T i 6|= ϕ or hH, T i |= ψ By abuse of notation, we use ‘|=’ both for classical and for HT-satisfaction: the ambiguity is removed by the form of the left interpretation (a single set T for classical and a pair hH, T i for HT). It is not difficult to see that, for total interpretations, hT, T i |= ϕ amounts to classical satisfaction T |= ϕ. Proposition 1. Any HT-interpretation hH, T i and any formula ϕ satisfy that hH, T i |= ϕ implies hT, T i |= ϕ (i.e. T |= ϕ classically).
HT-models can also be computed using Ferraris’ reduct [
A total interpretation hT, T i is an equilibrium model of a formula ϕ iff hT, T i |= ϕ and there is no H ⊂ T such that hH, T i |= ϕ. If so, we say that T is a stable model of ϕ. By Proposition 2 this means that T is a stable model of ϕ iff it is a minimal classical model of ϕT . We write SM[ϕ] to stand for the set of stable models of ϕ. Moreover, we represent their projection onto some vocabulary V as SMV [ϕ] d=ef { T ∩ V | T ∈ SM[ϕ] }.
Definition 1 (projective strong entailment/equivalence). Let ϕ and ψ be formulas and V some vocabulary (set of atoms). We say that ϕ V -strongly entails ψ, written ϕ |∼V ψ if SMV [ϕ ∧ γ] ⊆ SMV [ψ ∧ γ] for any formula γ such that At(γ) ⊆ V . We further say that ϕ and ψ are V -strongly equivalent, written ϕ V ψ, if both ϕ |∼V ψ and ψ |∼V ϕ, that is, SMV [ϕ ∧ γ] = SMV [ψ ∧ γ] for any formula γ such that At(γ) ⊆ V .
When the vocabulary V ⊇ At(ϕ) ∪ At(ψ) contains the original language
of ϕ and ψ, the projection has no relevant effect and the previous definitions
amount to regular (non-projective) strong entailment and strong equivalence. In
this case, we simply drop the V subindex in the previous notations. The following
results, respectively proved in [
In the case of projected strong entailment and equivalence, a semantic
characterisation was provided in [
In this section we consider an alternative characterisation of HT-semantics that relies on the idea of support for a given classical interpretation T . Definition 2 (T -support). 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 , ∅.
To increase readability of examples, we will 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 hH, T i |= ϕ. When H is empty [ ], there is no support for T , so hT, T i 6|= ϕ and thus, T is not even a classical model. If H is not empty, this means we have at least some model hH, T i and, by Proposition 1, hT, T i must be a model too; this is why we require T ∈ H in the set. When not empty, the fewer models in H, the more supported is T , since it is closer to being stable. Accordingly, the most supported H would precisely be H = [ T ] corresponding to a stable model. This ordering relation is formally defined below. Definition 3. Given a set T ⊆ At of atoms and two T -supports H and H0 we write H T H0 iff either H = [ ] or H ⊇ H0 , [ ].
We usually write H H0 instead of H T H0 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. We write HT to stand for the set of all possible T -supports. (HT , ) forms a poset whose bottom and top elements are [ ] and [ T ] respectively. Given a T -support H, we define its complementary support H as:
def H =
[ ] if H = 2T [ T ] ∪ {H ⊆ T | H < H} otherwise We also define HV as the projection of every set in H to the vocabulary V , i.e., def HV = {H ∩ V | H ∈ H}. The relation between T -supports and formulas is given by the following definition.
Definition 4 (T -denotation). Let T ⊆ At. The T -denotation of a formula ϕ, written ~ ϕ T , is a T -support recursively defined as follows: ~ ⊥ T d=ef [ ] ~ p T d=ef {H ⊆ T | p ∈ H} ~ ϕ ∧ ψ T d=ef ~ ϕ T ∩ ~ ψ T ~ ϕ ∨ ψ T d=ef ~ ϕ T ∪ ~ ψ T ~ ϕ → ψ T d=ef ( ~ ϕ T ∪ ~ ψ T otherwise
The following proposition follows by structural induction and shows that T -denotations can be used as an alternative semantics for the logic HT. Proposition 4. For any interpretation hH, T i and formula ϕ: hH, T i |= ϕ iff H ∈ ~ ϕ T .
Corollary 1. For any set T of atoms and propositional formulas ϕ, ψ, the following conditions hold: (i) T |= ϕ iff ~ ϕ T , [ ] iff T ∈ ~ ϕ T . (ii) T is a stable model of ϕ iff ~ ϕ T = [ T ]. (iii) Given H ⊆ T : H ∈ ~ ϕ T iff H |= ϕT .
The last item asserts that the denotation ~ ϕ T can also be seen as a
semantic counterpart of Ferraris’ reduct ϕT . The following result is a rephrasing of
Theorem 2 in [
Proposition 5. Let σ be an arbitrary assignment of a support σ(T ) ∈ HT for each T ⊆ At. Then, there exists a formula ϕ s.t. ~ ϕ T = σ(T ) for all T .
As an example, given At = {a, b}, the T -denotations of the formulas ¬a → b and a ∨ b are:
T ~ ¬a → b T
[ ] ∅ {a} [ ∅ {a} ] [ {a} ] {b} [ {b} ] [ {b} ] {a, b} [{a, b} {a} {b} ∅ ] [ {a, b} {a} {b} ] ~ a ∨ b T
[ ]
Notice that the only stable model of ¬a → b is {b} because ~ ¬a → b {b} = [{b}]. Similarly, the stable models of a ∨ b are {a} and {b}. Note also that, for all T , we always have ~ ¬a → b T ~ a ∨ b T , that is, ¬a → b is always less supported (further from being stable) than a ∨ b. In fact, this has an interesting consequence, as stated by the next result: Proposition 6. For any two propositional formulas ϕ, ψ the following hold: (i) ϕ |∼ ψ iff ~ ϕ T ~ ψ T for every set T ⊆ At of atoms, (ii) ϕ ψ iff ~ ϕ T = ~ ψ T for every set T ⊆ At of atoms.
While (ii) is an immediate consequence of Proposition 4, item (i) states that ϕ strongly entails ψ iff the former is always less supported than the latter. Note how Proposition 6 is much more readable than Proposition 3, especially regarding strong entailment and its relation to strong equivalence. In our example above, Proposition 6 implies that if we replace ¬a → b by a ∨ b in any program, we will get the same or perhaps more stable models. 4
A fork is defined using the grammar:
F ::= ⊥ p
F | F
F ∧ F ϕ ∨ ϕ ϕ → F where ϕ is a propositional formula and p ∈ At is an atom. As we can see, the fork operator ‘|’ cannot occur in the scope of disjunction or negation, since ¬F stands for F → ⊥ and implications do not allow forks in the antecedent. Extending the semantics to arbitrarily nested connectives is left for future work.
As we will see, a fork F will be always reducible to the form (ϕ1| . . . |ϕn) where each ϕi is a formula. Thus, a natural way to define its semantics is keeping a set of supports Δ = {H1, . . . , Hn} for each classical interpretation T . However, if we have a pair of supports in Δ such that Hi Hj , then Hi is useless since, according to Proposition 6 ii), if it yields a stable model, the latter is always produced by Hj too. For this reason, we will collect sets of supports that are -closed, so their maximal elements become the representative ones. Formally, given a T -support H we define the set of -smaller supports ↓H = {H0 ∈ HT | H0 H}. This is usually called the ideal of H. We extend this notation to any set of supports Δ so that ↓Δ d=ef SH∈Δ ↓H = { H0 H H ∈ Δ }. Definition 5 (T -view). A T -view is a non-empty set of T -supports Δ ⊆ HT that is -closed, i.e., ↓Δ = Δ.
Notice that, since a T -view Δ is not empty and -closed, the smallest T -support [ ] is always included in Δ. Therefore, {[ ]} is the smallest T -view with respect to set inclusion. Analogously, if the greatest T -support [ T ] is included in Δ, then Δ is precisely ↓[ T ]. We are now ready to extend the concept of T -denotation to forks. Definition 6 (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 hh F iiT , is a T -view recursively defined as follows:
T hh ⊥ ii hh p iiT d=ef {[ ]} d=ef ↓~ p T
for any atom p hh F ∧ G iiT d=ef ↓ { H ∩ H0
H ∈ hh F iiT and H0 ∈ hh G iiT } hh ϕ ∨ ψ iiT d=ef ↓{ H ∪ H0
H ∈ hh ϕ iiT and H0 ∈ hh ψ iiT } hh ϕ → F ii
T def
= hh F | G ii
T d=ef hh F iiT ∪ hh G ii
T ↓{ ~ ϕ T ∪ H {[ ]} if T |= ϕ and hh F iiT = {[ ]}
H ∈ hh F iiT } otherwise
It is easy to see that the fork operator ‘|’ is commutative, associative and idempotent. We will also see later that conjunction and implication distribute over ‘|’. As for the rest of operators, note that the definitions above also cover propositional formulas. The following result shows that this new T -denotation of a propositional formula ϕ as a T -view, hh ϕ iiT , is precisely the ideal of its T -denotation as a T -support ~ ϕ T .
Proposition 7. Let ϕ be a propositional formula and T ⊆ At be a set of atoms. Then, hh ϕ iiT = ↓~ ϕ T .
Corollary 2. Given a propositional formula ϕ, a set T ⊆ At of atoms is a stable model of ϕ iff hh ϕ iiT = ↓[ T ].
Corollary 2 provides a natural way to define stable models of forks. Definition 7. Given a fork F , we say that T ⊆ At is a stable model of F iff hh F iiT = ↓[ T ]. SM[F ] denotes the set of stable models of F .
The intuition behind a fork is that we can collect its stable models independently: Proposition 8. Given forks F and G: SM[F | G] = SM[F ] ∪ SM[G].
Once SM[F ] is defined, we can immediately extend the definition of V -strong entailment and equivalence to forks in the obvious way, i.e., using forks instead of propositional formulas. We postpone the effect of projecting onto some vocabulary V to the next section and focus on the regular, non-projected versions |∼ and . As in Proposition 6, |∼ and have a simple characterisation in terms of denotations: Proposition 9. For any pair of forks F, G the following hold: (i) F |∼ G iff hh F iiT ⊆ hh G iiT for every set T ⊆ At, (ii) F G iff hh F iiT = hh G iiT for every set T ⊆ At.
This helps us to derive the following interesting properties: Proposition 10. Let F, G, H be arbitrary forks and ϕ a formula. Then: (F | G) ∧ H ϕ → (F | G) (F ∧ H) | (G ∧ H) (ϕ → F ) | (ϕ → G) (F | G)
G if F |∼ G (1) (2) (3)
The first two properties (1) and (2), allow us to reduce any arbitrary fork to a normal form (ϕ1 | . . . | ϕn) where each ϕi is a propositional formula. Moreover, (3) is a kind of subsumption property that, without loss of generality, allows us to assume that no pair of formulas ϕi |∼ ϕj for i , j in that expression. As an example of subsumption, take the fork (¬a → b | a ∨ b). As we saw before, (¬a → b) |∼ (a ∨ b) because ~ ¬a → b T ~ a ∨ b T for all T (Proposition 6). Then, the ideal ↓~ ¬a → b T is included in ↓~ a ∨ b T which (by Proposition 7) is the same as saying hh ¬a → b iiT ⊆ hh a ∨ b iiT . But then, hh ¬a → b | a ∨ b iiT = hh ¬a → b iiT ∪ hh a ∨ b iiT = hh a ∨ b iiT . In other words, (¬a → b | a ∨ b) (a ∨ b).
An important consequence of conjunction-distributivity (1) is that, although ∧ is idempotent on propositional formulas, it ceases to be so when connecting forks. Take, for instance, the formalisation of Example 1 using the expression (a | b) ∧ (a | b). If we apply distributivity and reduce to a normal form: (a | b) ∧ (a | b) a ∧ (a | b) | b ∧ (a | b) distributivity (1) (a | a ∧ b) | (b ∧ a | b) distributivity (1), ∧ −idempotence a | a ∧ b | b ∧ a | b associativity of ‘|’ a | a ∧ b | b commut. of ∧ and idempotence of ‘|’ but then, by Proposition 8, from a ∧ b we get the stable model {a, b} < SM[a | b]. 5
In this section, we provide a semantic characterisation of projective strong entailment |∼V and equivalence V for some vocabulary V ⊆ At. We say that a T -support H is3 V -vacuous iff there is some H ⊂ T in H satisfying H ∩V = T ∩V . The reason for the name “vacuous” is that if we take a formula ϕ with denotation ~ ϕ T = H, then T will never become stable if we can only add a context γ for vocabulary V . To do so, we would need ~ ϕ ∧ γ T = [ T ] but H ⊂ T should also belong to the support since H and T are indistinguishable for any γ over V . Definition 8. 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 defined as follows:
T d=ef ↓ hh F iiV { HV
H ∈ hh F iiT 0 s.t. T 0 ∩ V = T and H is not V -vacuous }
In other words, we collect all the non-vacuous supports H that belong to any
T 0-denotation hh F iiT 0 such that T 0 coincides with T for atoms in V , and then we
3 This notion is analogous to condition ii) in the definition of V -SE-models that
characterises relativised strong equivalence [
More interestingly, the V -T -denotation of F can be used to precisely characterise its projected stable models.
Proposition 12. For any vocabulary V ⊆ At, fork F and set T ⊆ V of atoms, it holds that T ∈ SMV [F ] iff hh F iiVT = ↓[ T ].
As a main result, we naturally extend Proposition 9 to the projective case. Theorem 1. For any vocabulary V ⊆ At, forks F, G, the following hold: (i) F |∼V G iff hh F iiV ⊆ hh G iiVT for every set T ⊆ V of atoms, and
T (ii) F V G iff hh F iiVT = hh G iiVT for every set T ⊆ V of atoms.
Moreover, the following result shows that we can just use a formula as a context instead of an arbitrary fork.
Proposition 13. For any vocabulary V ⊆ At, forks F, G, the following hold: (i) F |∼V G iff SM[F ∧ γ] ⊆ SM[G ∧ γ] for any formula γ with At(γ) ⊆ V (ii) F V G iff SM[F ∧ γ] = SM[G ∧ γ] for any formula γ with At(γ) ⊆ V .
As an immediate consequence we can extend the characterisation of PSE
from disjunctive logic programs in [
T (ii) ϕ V ψ iff hh ϕ iiVT = hh ψ iiVT for every set T ⊆ V of atoms.
As we mentioned in the introduction, PSE is closely related to forgetting. Let At be a signature and V ⊆ At. Given a expression ϕ over At, a forgetting operator is a partial function f(ϕ, V ) = ψ that assigns a new expression ψ over4 V . Operator f is said to be strongly persistent iff ϕ V f(ϕ, V ) for every formula ϕ and set V ⊆ At of atoms for which it is defined. Now, imagine we wish to apply forgetting on a fork F over At keeping atoms V ⊆ At. In light of Corollary 3, we can start by obtaining the projected denotations hh F iiVT for all T ⊆ V . This corresponds to a set of T -views that can be precisely captured by another fork over V , as stated by the following result.
Proposition 14. Given a vocabulary V ⊆ At, and assignment σ so that σ(T ) is some arbitrary T -view for each T ⊆ V , there exists a fork G such that At(G) ⊆ V and hh G iiT = σ(T ) for all T ⊆ V . 4 Note that we are defining the forgetting operator with respect to the projected signature instead of the forgotten atoms At \ V .
In other words, we can always define f(F, V ) d=ef G by obtaining a fork G over V s.t. hh G iiT = hh F iiVT and, by Proposition 11 and Theorem 1, G V F . Theorem 2. For every fork F and set V ⊆ At of atoms, there is a fork G such that At(G) ⊆ V and F V G. Consequently, there is a total, strongly persistent forgetting operator over forks.
Recall from [
Proposition 15. Given sets T ⊆ V ⊆ At of atoms, then: (i) any formula ϕ with At(ϕ) ⊆ V satisfies hh ϕ iiVT = ↓~ ϕ T and, thus, hh ϕ iiTV has a -maximum element; (ii) for every T -view Δ with a -maximum element, there is a propositional T 0 = {[ ]} for formula ϕ with At(ϕ) ⊆ V that satisfies hh ϕ iiVT = Δ and hh ϕ iiV every T 0 ⊆ V with T 0 , T .
That is, there is a one-to-one correspondence between each assignment of T -views with some -maximum (i.e. unique maximal) element and a formula5 modulo strong equivalence in the vocabulary V . On the other hand, there are T -views that have more than one -maximal element and, thus, they cannot be represented as formulas. That is, there are more theories modulo V than theories over V modulo .
As an example, consider program Pm from the introduction interpreted as
the conjunction of its rules, and assume we want to forget ma and mb. Let us
take all s-umbasextimsTu m0⊆el{eam,ebn,tm, a~,Pmmb}T. 0S,isnhcoewPnministhaefolerfmtutalab,lealolfiFtsigTu0r-evi1ewwshewriel,l
have a
for brevity, we only show cases of non-empty supports (i.e., when T 0 is a classical
model). Observe that none of these supports is V -vacuous because we never get a
strictly smaller H ⊂ T that coincides with T in V = {a, b}. Now, according to the
definition of hh Pm iiVT , for each T ⊆ V = {a, b} we must find those T 0 such that
T 0 ∩ {a, b} = T . For T = {a} the only possibility is T 0 = {ma, a} that, after
removing ma, yields a maximum support [{a}]. The case for T = {b} is completely
symmetric, yielding maximum support [{b}]. But for T = {a, b} we get three
candidate interpretations, T10 = {ma, a, b}, T20 = {mb, a, b} and T30 = {ma, mb, a, b}.
A first observation is that the support for T30 = {ma, mb, a, b} is {a, b}-vacuous,
since it contains {ma, a, b} and {mb, a, b} that coincide with T30 for atoms {a, b}.
After removing ma, mb in the supports of the non-vacuous candidates, T10 and
T20, the respective results are [ {a, b} {a} ] and [ {a, b} {b} ] that are not
comparable. Therefore, they become the two -maximal supports in the T -view
5 A way to obtain the formula is collecting the set of HT-countermodels (those not in
the T -supports) and applying the method in [
T
maximal supports in hh P2 iiT {a} [ {a} ] {b} [ {b} ] {a, b} [ {a, b} ] as the three cases are stable models. But this means that each T -view has a -maximum T -support, and so, the fork is representable as a formula. Program P1 has precisely the same T -views, so it is strongly equivalent to P2. T
T max. supports in hh Pm iiV {a} [ {a} ] {b} [ {b} ] {a, b} [ {a, b} {b} ] [ {a, b} {a} ]
T 0 {ma, a} {mb, b} {ma, a, b} {mb, a, b} max. supports in hh Pm iiT 0 [ {ma, a} ] [ {mb, b} ] [ {ma, a, b} {ma, a} ] [ {mb, a, b} {mb, b} ] {ma, mb, a, b} [ {ma, mb, a, b} {mb, a, b} {mb, b} {ma, a, b} {ma, a} ]
To illustrate a case not requiring forks, take a second example α = (¬p → q) ∧ (¬q → p) and assume we want to forget q. The maximal (non-empty) supports in the views of α are:
maximal supports in hh α iiT 0 {p} [ {p} ] {q} [ {q} ] {p, q} [ {p, q} {p} {q} ∅ ] Note now that the last support is {p}-vacuous because {p} ⊂ {p, q} = T 0 but they coincide in the truth of V = {p}. Thus, for T = {p} we only have the non-vacuous T 0 = {p} and we get [{p}] as maximum support. For T = ∅ we have T 0 = {q} and, after removing atom q, we obtain [∅] as maximum support. As both views have maximum supports, this is representable as a propositional formula, that in this case corresponds to the choice p ∨ ¬p or, if preferred, ¬¬p → p.
We have extended the syntax and semantics of Here-and-There (HT) to deal with
a new type of construct ‘|’ called fork. We have 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 [
Our work on PSE is strongly related to [
For future work, we plan to extend these results to other characterisations of
equivalence [
Acknowledgements. We are especially thankful to the anonymous reviewers for their helpful suggestions to improve the paper.