Introduction

Logic programming (LP) under answer set semantics is a declarative non-monotonic reasoning formalism with a robust theoretical (and monotonic) foundation based in intuitionistic logic [1]. In essence, answer sets (which are sometimes referred to as stable models) are a second-order notion over classical formulas [2], providing more expressive power than first-order logic, making it possible, for example, to identify Hamiltonian cycles [3].

The question of how a program may be simplified is not simply answered. The surge of research around it, rather suggests that it is very nuanced, where the limits and possibilities vary greatly, depending on the exact definition of what is meant by being simpler, and the concrete formalism that is being investigated. Such processes might find application, e.g. in a legal context; in order to exclude dependencies that are no longer deemed relevant; or to reduce the complexity of reasoning tasks.

Forgetting [4,5,6], or variable elimination, which is one such possible interpretation of simplification, intuitively means that a programs signature is restricted, while the logical dependencies of the remaining atoms are left unchanged. It has been considered with respect to many properties including strong persistence pSPq which seemingly captures best its intuitions [7]. In essence, pSPq ensures that the result of forgetting atoms 𝑉 from a program 𝑃 exerts the same behavior as 𝑃 under the addition of a context program 𝑅 not containing any forgotten atoms. There are instances for which pSPq is impossible to be achieved [8]. Following this negative result, several relaxations of pSPq were proposed, which are attainable through different semantic means [9,10,11].

While results of forgetting using the desired semantics may be obtained by counter-model construction [12] and perhaps be minimized using a version of the Quine-McCluskey algorithm [13], a much more direct and conservative approach is to forget by syntactically manipulating an input program. There are several such syntactical operators in the literature [14,15,16,17,18,19,20], where notably f SP , as its name suggests, satisfies pSPq whenever possible. Already, it is impossible to satisfy pSPq [8]. However, a possible result satisfying a relaxation of pSPq may be [17]:

𝑎 _ 𝑏 Ð 𝑏 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑏 𝑎 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎

where 𝑎 and 𝑏 each support themselves, and at least one of them is true. The fact that forgetting in practice should not be done by hand, is probably best witnessed by the fact that forgetting about multiple atoms may not be reduced to forgetting them in iteration. Rather, the result is derived by a recursive derivation tree [19]. 1 Abstraction by omission [21,22,23] can be seen as a relaxed version of forgetting, where atoms are removed from a program, but its answer-sets are only required to behave as before, under no addition of another program 𝑅.

The aptly named Simplification [24] reduces the signature of a program 𝑃 by a set of atoms 𝐴 as well, requiring the result to behave the same as 𝑃 under a context program 𝑅 that may contain atoms 𝐴 in a restricted way.

These different ideas as well as several versions of equivalence were recently captured by an overarching notion of 𝐴-simplifications of 𝑃 relative to 𝐵, where 𝐴 is a set of atoms that is to be removed, and 𝐵 is the signature of possible context programs 𝑅 [25]. Interestingly, by taking into account the full spectrum of all of these ideas, a novel, relaxed version of pSPq, so-called relativized Strong Persistence prSPq emerged.

What is missing from the picture now, is a concrete syntactic transformation f rSP that satisfies prSPq, whenever possible. Since pSPq and prSPq coincide in some cases, it is clear that we should start our search at f SP and see how we get to f rSP from there. While the question this paper is out to answer may appear simple at first, its answer is far from it. To be able to construct f rSP , it turns out that it is necessary to intrically modify sub-procedures of f SP . Finally, with this operator at our disposal, we are then able to construct syntactically general 𝐵-relativized 𝐴-simplifications.

Given that the class of forgetting operators F rSS to satisfy prSPq, whenever possible, is defined methodologically to meet this criterion, and that the operator f rSP is defined methodologically to match F rSS , we assume any intuition about the derivation rules one may find to be 'post hoc'. We therefore leave the task of finding an intuitive explanation of why they are as they are for future studies.

Background

Given that F rSS and therefore f rSP require the understanding of several topics that are 'non-canon' and scientific papers should be self-contained there is a surprising amount of research to be recalled, in spite of the fact that the topic of this paper is forgetting. Therefore, after recalling the foundations of logic programming, we compile and streamline a rather long list of definitions and results from the literature. Logic Programs. We assume a propositional signature Σ. A logic program 𝑃 over Σ is a finite set of rules of the form 𝑎1 _ . . . _ 𝑎 𝑘 Ð 𝑏1, . . . , 𝑏 𝑙 , 𝑛𝑜𝑡 𝑐1, . . . , 𝑛𝑜𝑡 𝑐𝑚, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑1, . . . , 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑𝑛, where all 𝑎1, . . . , 𝑎 𝑘 , 𝑏1, . . . , 𝑏 𝑙 , 𝑐1, . . . , 𝑐𝑚, and 𝑑1, . . . , 𝑑𝑛 are atoms of Σ [26]. Such rules 𝑟 are also written more succinctly as

H p𝑟q Ð B `p𝑟q, 𝑛𝑜𝑡 B ´p𝑟q, 𝑛𝑜𝑡 𝑛𝑜𝑡 B ´´p𝑟q,

where H p𝑟q " t𝑎1, . . . , 𝑎 𝑘 u, B `p𝑟q " t𝑏1, . . . , 𝑏 𝑙 u, B ´p𝑟q " t𝑐1, . . . , 𝑐𝑚u, and B ´´p𝑟q " t𝑑1, . . . , 𝑑𝑛u, and we will use both forms interchangeably. Given a rule 𝑟, H p𝑟q is called the head of 𝑟, and B p𝑟q " B `p𝑟q Y 𝑛𝑜𝑡 B ´p𝑟q Y𝑛𝑜𝑡 𝑛𝑜𝑡 B ´´p𝑟q is called the body of 𝑟, where, for a set 𝐴 of atoms, 𝑛𝑜𝑡 𝐴 " t𝑛𝑜𝑡 𝑞 | 𝑞 P 𝐴u and 𝑛𝑜𝑡 𝑛𝑜𝑡 𝐴 " t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞 | 𝑞 P 𝐴u.

Σp𝑃 q and Σp𝑟q denote the set of atoms appearing in 𝑃 and 𝑟, respectively.

Given a program 𝑃 and an interpretation, i.e., a set 𝐼 Ď Σ of atoms, the reduct of 𝑃 given 𝐼, is defined as 𝑃 𝐼 " tH p𝑟q Ð B `p𝑟q | 𝑟 P 𝑃 such that B ´p𝑟q X 𝐼 " H and B ´´p𝑟q Ď 𝐼u. An HT-interpretation is a pair x𝑋, 𝑌 y s.t. 𝑋 Ď 𝑌 Ď Σ. Given a program 𝑃 , an HT-interpretation x𝑋, 𝑌 y is an HT-model2 of 𝑃 , x𝑋, 𝑌 y |ù 𝑃 , iff 𝑌 |ù 𝑃 and 𝑋 |ù 𝑃 𝑌 , where |ù both denotes the standard satisfaction relation for classical logic and for HT-logic. 3 An HT-interpretation x𝑋, 𝑌 y is total iff 𝑋 " 𝑌 . Given a rule 𝑟, x𝑋, 𝑌 y |ù 𝑟, iff x𝑋, 𝑌 y |ù t𝑟u. We admit that the set of HT-models of a program 𝑃 is restricted to Σp𝑃 q even if Σp𝑃 q Ă Σ. We denote by ℋ𝒯 p𝑃 q the set of all HT-models of 𝑃 . A set of atoms 𝑌 is an answer set of 𝑃 iff x𝑌, 𝑌 y P ℋ𝒯 p𝑃 q, and there is no 𝑋 Ă 𝑌 such that x𝑋, 𝑌 y P ℋ𝒯 p𝑃 q. We term HT-models x𝑋, 𝑌 y s.t. 𝑋 Ă 𝑌 witnesses. The set of all answer sets of 𝑃 is denoted by 𝒜𝒮p𝑃 q. Two programs 𝑃1, 𝑃2 are equivalent iff 𝒜𝒮p𝑃1q " 𝒜𝒮p𝑃2q and strongly equivalent, 𝑃1 " 𝑃2, iff 𝒜𝒮p𝑃1 Y 𝑅q " 𝒜𝒮p𝑃2 Y 𝑅q for any program 𝑅. It is well-known that 𝑃1 " 𝑃2 exactly when ℋ𝒯 p𝑃1q " ℋ𝒯 p𝑃2q [27]. Given a set 𝑉 Ď Σ, the 𝑉 -exclusion of a set of answer sets (a set of HT-interpretations) ℳ, denoted ℳ ‖𝑉 , is t𝑋z𝑉 | 𝑋 P ℳu (tx𝑋z𝑉, 𝑌 z𝑉 y | x𝑋, 𝑌 y P ℳu).

Forgetting: Properties and Operators. Let 𝒫 be the set of all logic programs. A forgetting operator is a (partial) function f : 𝒫 ˆ2Σ Ñ 𝒫. The program fp𝑃, 𝑉 q is interpreted as the result of forgetting about 𝑉 from 𝑃 . Moreover, Σpfp𝑃, 𝑉 qq Ď Σp𝑃 qz𝑉 is usually required. In the following we introduce some well-known properties for forgetting operators [8].

Strong persistence is presumably the best known one [16]. It requires that the result of forgetting fp𝑃, 𝑉 q is strongly equivalent to the original program 𝑃 , modulo the forgotten atoms.

pSPq f satisfies strong persistence iff, for each program 𝑃 and each set of atoms 𝑉 , we have: 𝒜𝒮p𝑃 Y𝑅q ‖𝑉 " 𝒜𝒮pfp𝑃, 𝑉 qY𝑅q for all programs 𝑅 with Σp𝑅q Ď Σ\𝑉 .

Notably, pSPq can be decomposed into the following three properties, i.e. an operator f satisfies pSPq iff f satisfies all pwCq, psCq and pSIq, where pwCq f satisfies weakened consequence iff, for each 𝑃 and each set of atoms 𝑉 : 𝒜𝒮pfp𝑃, 𝑉 qq Ě 𝒜𝒮p𝑃 q ‖𝑉 . psCq f satisfies strengthened consequence iff, for each 𝑃 and each set of atoms 𝑉 : 𝒜𝒮pfp𝑃, 𝑉 qq Ď 𝒜𝒮p𝑃 q ‖𝑉 .

Strong invariance requires that rules not mentioning atoms to be forgotten can be added before or after forgetting.

pSIq f satisfies strong invariance iff, for each program 𝑃 and each set of atoms 𝑉 , we have: fp𝑃, 𝑉 q Y 𝑅 " fp𝑃 Y 𝑅, 𝑉 q for all programs 𝑅 with Σp𝑅q Ď Σz𝑉 .

Note that the presented properties are often considered for certain subclasses such as disjunctive, normal or Horn programs. Moreover, they naturally extend over classes of forgetting operators, where a class satisfies a property, iff all its members do.

In the light of the impossibility for a forgetting operator to satisfy pSPq for all pairs x𝑃, 𝑉 y, called forgetting instances, where 𝑃 is a program and 𝑉 is a set of atoms to be forgotten from 𝑃 [8], pSPq was defined for concrete forgetting instances. A forgetting operator f satisfies pSPq x𝑃,𝑉 y , if 𝒜𝒮pfp𝑃, 𝑉 q Y 𝑅q " 𝒜𝒮p𝑃 Y 𝑅q ‖𝑉 , for all programs 𝑅 with Σp𝑅q Ď Σ\𝑉 . A sound and complete criterion Ω characterizes when it is not possible to forget while satisfying pSPq x𝑃,𝑉 y . Corresponding to the Ω criterion the classes F R and F SP specify the HT-models of the forgetting result. It was shown that F SP satisfies pSPq x𝑃,𝑉 y for all instances x𝑃, 𝑉 y that do not satisfy Ω. Moreover, in the case where Ω is satisfied, F SP still exhibits desirable behavior, such as satisfying pSIq and pwCq, two of three characterizing criterions of pSPq. F R on the other hand always satisfies psCq and pSIq, which makes it an ideal choice, if no new answer sets should be created [9].

The classes F R and F SP are defined as follows:

F R :" tf | ℋ𝒯 pfp𝑃, 𝑉 qq " tx𝑋, 𝑌 y | 𝑌 Ď Σp𝑃 qz𝑉 ^ 𝑋 P ď ℛ 𝑌 x𝑃,𝑉𝑅 ||𝐴 :" tH p𝑟q Ð B p𝑟qzp𝐴 Y 𝑛𝑜𝑡 𝑛𝑜𝑡 𝐴q | pH p𝑟q Y B `p𝑟qq X 𝐴 " Hq, 𝑟 P 𝑅u 𝑃 is strong 𝐴-simplifiable if there is such a 𝑄.

Theorem 2.4 (Saribatur and Woltran (2023)). If pro-

gram 𝑃 is strongly 𝐴-simplifiable, then 𝑃 ||𝐴 is a strong 𝐴-simplification of 𝑃 .

Relativized (Strong) Simplification.

Recently simplifications have been relaxed to take into account relativized equivalence, i.e. s.t. the simplification 𝑄 of 𝑃 only needs to stay equivalent under addition of any 𝑅 over a relativized signature 𝐵 Ď Σ.

Definition 2.5 (Woltran (2004)). A pair of interpretations x𝑋, 𝑌 y is a (relativized) B-HT-interpretation iff either 𝑋 " 𝑌 or 𝑋 Ă p𝑌 z𝐵q. The former are called total and the latter nontotal B-HT-interpretations. Moreover, a B-HT-interpretation x𝑋, 𝑌 y is a (relativized) B-HT-model of a program 𝑃 iff:

1. 𝑌 |ù 𝑃 ; 2. for all 𝑌 1 Ă 𝑌 with p𝑌 1 z𝐵q " p𝑌 z𝐵q :

𝑌 1 |ù 𝑃 𝑌 ; and 3. 𝑋 Ă 𝑌 implies existence of a 𝑋 1 Ď 𝑌 with 𝑋 1 z𝐵 " 𝑋, such that 𝑋 1 |ù 𝑃 𝑌 holds.

The set of B-HT-models of 𝑃 is given by ℋ𝒯 𝐵 p𝑃 q. Two programs 𝑃1 and 𝑃2 are strongly equivalent relative to 𝐵 iff ℋ𝒯 𝐵 p𝑃1q " ℋ𝒯 𝐵 p𝑃2q.

Definition 2.6 (Saribatur and Woltran (2024)).

Given 𝑃 over Σ, 𝐴, 𝐵 Ď Σ, and 𝑄 over Σz𝐴, 𝑄 is a (strong) 𝐴-simplification of 𝑃 relative to 𝐵 if for any program 𝑅 over 𝐵 that is 𝐴-separated:

𝒜𝒮p𝑃 Y 𝑅q ||𝐴 " 𝒜𝒮p𝑄 Y 𝑅 ||𝐴 q Program 𝑃 is 𝐵-relativized (strong) 𝐴-simplifiable if there is such a 𝑄.

The relativized equivalence can similarly be taken into account in forgetting. The following theorem confirms that forgetting can be used as a stepping-stone to, more generally, derive 𝐵relativized 𝐴-simplifications.

Definition 2.7 (Saribatur and Woltran (2024)). A forgetting operator

Theorem 2.14 (Saribatur and Woltran (2024)).

Let 𝑃 be 𝐵-relativized 𝐴-simplifiable, and f P F rSS . Then fp𝑃 ||𝐴X𝐵 , 𝐴z𝐵, 𝐵z𝐴q is a 𝐵-relativized 𝐴-simplification of 𝑃 .

Syntactic Tools

Defining a syntactic forgetting operators that obeys the semantics of F rSP inevitably comes down to modifying the existing operator f SP 5 , which is why we recall it and its auxiliary constructions. For succinctness, for examples of established definitions, we refer to [19].

As usual [29,30,13,31,16,17] A program 𝑃 is in normal form iff 𝑁 𝐹 p𝑃 q " 𝑃 .

The 𝑞-exclusion notation is shorthand to remove an atom.

Definition 2.18 (𝑞-exclusion Berthold (2022)).

Given an atom 𝑞 P Σ, and a set of literals 𝐿, a rule 𝑟 and a program 𝑃 over Σ, the 𝑞-exclusions are 𝐿 z𝑞 :" 𝐿zt𝑞, 𝑛𝑜𝑡 𝑞, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞u, 𝑟 z𝑞 :" H z𝑞 p𝑟q Ð B z𝑞 p𝑟q and 𝑃 z𝑞 :" t𝑟 z𝑞 | 𝑟 P 𝑃 u.

We define a partition of a program along the occurrences of a given atom 𝑞. There are some correspondences between the models of a program and its rules that we can spot by this partitioning. The as-dual construction [17] generalizes constructions that collect sets of conjunctions of literals aiming to replace negated occurrences of a literal [15,16] The product of rules and programs are defined in order to unite their models.

Definition 2.23 (Product of Rules Berthold (2022)).

Let 𝑟1 and 𝑟2 be rules. Their product 𝑟1 ˆ𝑟2, is defined as: The double negation of a rule is such, to be able to reason about, whether the second item 𝑌 of an HT-model x𝑋, 𝑌 y is a classical model, and therefore whether the corresponding total model x𝑌, 𝑌 y is a potential answer set. We would like to point out that similarly, a formula 𝜓 holds classically iff "" 𝜓 holds intuitionistically. This connection is little surprising, given that HT-logic lies between classical and intuitionistic logic [27]. Further, if we extend the definition of double negation over programs, i.e. 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃 :" t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 | 𝑟 P 𝑃 u, we are able to construct a program that unites the HT-models of two programs:

H p𝑟1q Y H p𝑟2q Ð B p𝑟1q Y Bℋ𝒯 p𝑃1q Y ℋ𝒯 p𝑃2q " ℋ𝒯 pp𝑃1 Y 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃1q ˆp𝑃2 Y 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃2qq.

Any rule 𝑟 subsumes 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟. In order not to lose double negated rules, we therefore restrict the normal form construction 𝑁 𝐹 to its first three steps, denoted 𝑛𝑓 , when necessary.

We will also tweak subsumption, since as it is defined above it has some properties that make it impractical to use. For one, it is not anti-symmetrical, two syntactically different rules may subsume each other, such as: 𝑟1 :" Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎 and 𝑟2 :" Ð 𝑎, where 𝑟1 ď 𝑟2 and 𝑟2 ď 𝑟1.

Moreover, even though a rule may subsume another rule, this relation may break, when both of them are conjoined by ˆwith the same third rule, e.g. let 𝑟3 :" 𝑏 Ð, then

𝑟1 ˆ𝑟3 " 𝑏 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎 ă 𝑏 Ð 𝑎 " 𝑟2 ˆ𝑟3.

To avoid these issues, we define a stricter version of subsumption.

Definition 2.29. Given two fundamental rules 𝑟 and 𝑠, 𝑠 strongly subsumes 𝑟, in symbols 𝑠 ď𝑠 𝑟, iff:

1. H p𝑠q Ď H p𝑟q Y B ´p𝑟q, 2. B `p𝑠q Ď B `𝑠 ď𝑠 𝑟 ñ 𝑠 ď 𝑟 (1)

Strong subsumption is anti-symmetric:

𝑠 ď𝑠 𝑟 ^𝑟 ď𝑠 𝑠 ñ 𝑠 " 𝑟. (2)

Strong subsumption is a greatest subset of regular subsumption, to be anti-symmetric and transitive:

𝑠 ă 𝑟 ñ 𝑠 ă𝑠 𝑟 (3) 𝑠 ď𝑠 𝑟 ^𝑟 ď𝑠 𝑡 ñ 𝑠 ď𝑠 𝑡. (4)

Strong subsumption is preserved under ˆ:

𝑠 ď𝑠 𝑟 ñ 𝑠 ˆ𝑡 ď𝑠 𝑟 ˆ𝑡 for all rules 𝑡.

(

)5

As a consequence, strong subsumption is 'modular' in the following sense:

𝑠 ď𝑠 𝑟 ô @𝐴 Ď Σ : 𝑠 z𝐴 ď𝑠 𝑟 z𝐴 .(6)

Proof:𝑃 ‰ 𝑁 𝑃 p1q The requirement for ď𝑠 is stricter than that of ď. p2q Follows from basic set theory and the fact that 𝑠 and 𝑟 are fundamental, and therefore H p𝑡q X B ´p𝑡q " H " B `p𝑡q X B ´´p𝑡q for 𝑡 P t𝑠, 𝑟u. p3q The requirement for ď𝑠 is stricter than that of ď. p4q The subset relation is transitive. p5q Adding literals to either part of 𝑠 and 𝑟 has no effect on the required subset-relationship. p6q Is a consequence of p5q.

A rule 𝑟 is minimal in 𝑃 , iff it is not strongly subsumed by another rule 𝑠 in 𝑃 , i.e. iff ␣D𝑠 P 𝑃 : 𝑠 ă𝑠 𝑟.

All the aforementioned correspondences between models and rules remain, when an atom 𝑞 is removed from a rule as well as from an interpretation. The rules identified in Prop. 2.31 constitute the essential pillars of defining forgetting operators.

Syntactic Forgetting with pSPq

Given that the semantics of F rSP and F SP coincide for some inputs, it is not surprising that a representative of F rSP needs to be a modification of f SP . We, hence, recall its construction [19]. The operator f SP is defined via two auxiliary operators f R and f W , each of which is again defined using auxiliary operators f 𝐴 R and f 𝐴 W , which are defined inductively. Then:

f Ŕ p𝑃, 𝑞q :" 𝑛𝑓 p1 Y 2q

where:

1 :" t𝑟 1z𝑞 | 𝑟 1 P 𝑅 Y 𝑅1 Y 𝑅4u 2 :" t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 1z𝑞 | 𝑟 1 P 𝑅1 Y 𝑅4u

The operators f 𝐴 R is defined inductively by nested calls on f R and f Ŕ . In order to fix a concrete forgetting result, we assume an arbitrary order on 𝑉 , which has no effect on the following propositions.

Definition 2.35 (f 𝐴

R Let 𝑃 be a program over Σ, and 𝐴 Ď t𝑞1, 𝑞2, . . . , 𝑞𝑛u " 𝑉 Ď Σ, s.t. 0 ă 𝑛, then:

f 𝐴 R p𝑃, Hq :" 𝑃 f 𝐴 R p𝑃, 𝑉 q :" f b𝑛 R pf 𝐴 z𝑞𝑛 R p𝑃, 𝑉 zt𝑞𝑛uq, 𝑞𝑛q

where:

f b𝑛 R :" # f R , if 𝑞𝑛 P 𝐴 f Ŕ ,f 𝐴 W p𝑃, Hq :" 𝑃 f 𝐴 W p𝑃, 𝑉 q :" f b𝑛 W pf 𝐴 z𝑞𝑛 W p𝑃 z𝑅, 𝑉 zt𝑞𝑛uq, 𝑞𝑛q Y 𝑅

where:

f b𝑛 W :" # f Ẁ , if 𝑞𝑛 P 𝐴 f Ẃ ,f W p𝑃, 𝑉 q :" 𝑁 𝐹 p ď 𝐴Ď𝑉 f 𝐴 W p𝑃, 𝑉 qq Definition 2.44 (f SP ). Let 𝑃 be a program over Σ in normal form and 𝑉 Ď Σ. f SP p𝑃, 𝑉 q :" 𝑁 𝐹 pf W p𝑃, 𝑉 q Y f R p𝑃, 𝑉 qq

Example 2.45. Let 𝑃2.45 " t𝑎 Ð 𝑏, 𝑞; 𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑞; 𝑞 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞u, and 𝑉 " t𝑝, 𝑞u. Then f SP p𝑃, 𝑉 q can be derived by:

f t𝑞u R p𝑃, 𝑉 q Ď t𝑐 Ð 𝑑u f t𝑞u W p𝑃, 𝑉 q " t𝑎 Ð 𝑏, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎u f H R p𝑃, 𝑉 q Ď t𝑎 Ð 𝑏u f H W p𝑃, 𝑉 q " t𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑐u f SP p𝑃, 𝑉 q " 𝑁 𝐹 pf t𝑞u R p𝑃, 𝑉 q ˆfH R p𝑃, 𝑉 q Y f t𝑞u W p𝑃, 𝑉 q Y f H W p𝑃, 𝑉 qq " t𝑎 _ 𝑐 Ð 𝑏, 𝑑; 𝑎 Ð 𝑏, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎; 𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑u Theorem 2.46. f SP P F SP

Towards Syntactic Forgetting with prSPq

The idea in the following constructions is to modify the results of the previous operators, to take into account a set 𝐵 to relativize to. As witnessed in the previous section, half of the construction of f SP is a member of another class F R . We define a relaxation F rR of this class too, to aim for first.

F rR :" tf | ℋ𝒯 𝐴,𝐵 pfp𝑃, 𝐴, 𝐵qq " tx𝑋, 𝑌 y | 𝑌 Ď Σz𝑉 ^𝑋 P ď ℛ 𝑌

x𝑃,𝐴,𝐵y u, for all programs 𝑃 and 𝐴, 𝐵 Ď Σu While the 'r' in prSPq and the 'R' in F R both mean 'relativized', it is not clear in which sense F R corresponds to the idea of relativized equivalence. Still we use the subscript 'rR' for this new class in reference to its origin in F R .

Assume a program 𝑃 over Σ, 𝑉, 𝐵 Ď Σ, s.t. 𝑉 X 𝐵 " H, and 𝑌 Ď 𝐵. If we take a look at the definition of the class F rR , we can note that there is a similarity in how it treats forgotten atoms 𝑉 and atoms that it relativizes from Σp𝑃 qz𝐵: The operator f R includes an encoding for the first bulletpoint. The key-idea therefore is to manipulate the auxiliary constructions of f R further, to encode the second bulletpoint.

• Given 𝐴 Ď 𝑉 ,

For each 𝐴 Ď 𝑉 and 𝐶 Ď Σp𝑃 qzp𝐵 Y 𝑉 q, we define an auxiliary operator g 𝐴,𝐶 R that determines for any 𝑌 Ď pΣp𝑃 q X 𝐵qz𝑉 whether (i) 𝑌 Y 𝐴 Y 𝐶 |ù 𝑃 , and whether (ii) there are no 𝐴 1 Ď 𝐴 and 𝐶 1 Ď 𝐶, s.t. 𝐴 1 Y 𝐵 1 Ă 𝐴 Y 𝐵, and x𝑌 𝐴 1 𝐶 1 , 𝑌 𝐴𝐶y |ù 𝑃 . Then g 𝐴,𝐶 R p𝑃, 𝑉 q, satisfies x𝑌 𝐶, 𝑌 𝐶y, iff (i) and (ii). Further, we let g 𝐴,𝐶 R p𝑃, 𝑉 q contradict each x𝑋𝐶 2 , 𝑌 𝐶y with 𝑋 Ă 𝑌 , 𝐶 2 Ď 𝐶, iff 𝑃 |ù x𝑌 𝐴 1 𝐶 1 , 𝑌 𝐴𝐶y for all 𝐴 1 Ă 𝐴 and 𝐶 1 Ă 𝐶.

The operators g 𝐴,𝐶 R are defined taking into account f 𝐴 R as a baseline, i.e. g 𝐴,𝐶 R p𝑃, 𝑉, 𝐵q :" g 𝐶 R pf 𝐴 R p𝑃, 𝑉 q, 𝐵q. These g 𝐶 R we define inductively, starting at |𝐶| " 1.

Definition 3.1 (g R ).

Given a program 𝑃 in normal form over Σ and 𝑐 P Σ s.t. occp𝑃, 𝑐q " x𝑅, 𝑅0, 𝑅1, 𝑅2, 𝑅3, 𝑅4y. Then:

g R p𝑃, 𝑐q :" 𝑛𝑓 p1 Y 2 Y 3 Y 4 Y 5q

where: The building-blocks g Ẁ and g Ẃ of our inductive definition take into account one atom that is relativized away. We can therefore again use the observations of Prop. 2.31 We would like to remark here that, while this construction may appear rather costly computationally, some factors that may dampen the blow-up that have been discussed in nonrelativized forgetting [19], also apply here.

1 :" tÐ 𝐷 | 𝐷 P 𝒟 𝑐 𝑎𝑠 p𝑅3 Y 𝑅4qu 2 :" t𝑟 | 𝑟 P 𝑅 Y 𝑅2u 3 :" t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 | 𝑟 P 𝑅0 Y 𝑅2u 4 :" t𝑟 1 | 𝑟 1 P 𝑅3 Y 𝑅4u 5 :" tÐ 𝑛𝑜𝑡 𝑐u

Most importantly, the operator g 𝐴,𝐶 W is such that its result is the empty program, if the combination 𝐴, 𝐶 is 'nonrelevant'. If this 'non-relevancy' is detected within a recursive step of g 𝐴,𝐶 W possibly exponentially many calculations can be disregarded.

More concretely, assume for example a program 𝑃 over t𝑎, . . . , 𝑧u, 𝑉 " t𝑝, . . . , 𝑧u and 𝐵 " t𝑎, . . . , ℎu. If f Ẁ p𝑃, 𝑝q " H, then g 𝐴,𝐶 W p𝑃, 𝑉, 𝐵q will be the empty program for any 𝐴 Ě t𝑝u and any 𝐶, which lets us disregard a large part of the recursive calculation-tree. f rSP p𝑃, 𝑉 q :" 𝑁 𝐹 pg W p𝑃, 𝑉 q Y g R p𝑃, 𝑉 qq Theorem 4.9. f rSP P F rSS Corollary 4.10. Let 𝑃 be 𝐵-relativized 𝐴-simplifiable, then f rSP p𝑃 ||𝐴X𝐵 , 𝐴z𝐵, 𝐵q is a 𝐵-relativized 𝐴-simplification of 𝑃 .

Let's not Forget about Predicates

It remains an open question, as to how forgetting propositional atoms from a program translates to the more general case of forgetting from a program with variables. As has been done for classical formulas [4] one may consider forgetting about terms, ground atoms, or predicate symbols, where the latter probably comes closest to the propositional case. When forgetting about predicate symbols, two obstacles come to mind. (i) A predicate may be recursive, making it impossible to find a (finite) forgetting result. E.g.: consider forgetting 𝑡 from the following program: 𝑡p𝑋, 𝑌 q Ð 𝑒p𝑋, 𝑌 q.

𝑎p𝑋, 𝑌 q Ð 𝑡p𝑋, 𝑌 q, 𝑏p𝑋, 𝑌 q.

𝑡p𝑋, 𝑍q Ð 𝑡p𝑋, 𝑌 q, 𝑒p𝑌, 𝑍q.

One may consider finite forgetting results that have desirable properties up to some bound, as has been similarly done for classical logic [32]. (ii) Even if a non-recursive predicate symbol is forgotten we may have to leave the class of logic programs to represent a result of forgetting. E.g. consider forgetting about about 𝑏 from the following program where 𝑏 marks all pairs which are connected through two edges:

𝑏p𝑋, 𝑍q Ð 𝑒p𝑋, 𝑌 q, 𝑒p𝑌, 𝑍q. 𝑛p𝑋q Ð 𝑒p𝑋, 𝑌 q.

𝑎p𝑋, 𝑌 q Ð 𝑛𝑜𝑡 𝑏p𝑋, 𝑌 q, 𝑛p𝑋q, 𝑛p𝑌 q. 𝑛p𝑌 q Ð 𝑒p𝑋, 𝑌 q.

A possible forgetting result in full first order syntax is 𝜓: @𝑋, 𝑍 : p␣D𝑌 : p𝑒p𝑋, 𝑌 q ^𝑒p𝑌, 𝑍qq ^𝑛p𝑋q ^𝑛p𝑌 q Ñ 𝑎p𝑋, 𝑍q ^𝑒p𝑋, 𝑍q Ñ p𝑛p𝑋q ^𝑛p𝑍qqq where the impossiblility of 𝜓 to be put into a prenexnormalform, is inherited from intuitionism. It may be worthwhile to consider subclasses of the full first-order syntax that are well behaved w.r.t. forgetting. Related to this question there are two extensions of logic programs that are able to capture the full polynomial hierarchy, stable-unstable programs [33] and logic programs with quantifiers [34]. A relaxed version of forgetting from logic programs, so-called interpolation has recently been successfully reduced to the classical case [35].

Conclusion

The question on how a logic program may be simplified, has become a rather large one, sparking several subtopics that cover different particular aims: forgetting, abstraction, simplification. These ideas have recently been captured under an umbrella-term of (strong) 𝐴-simplifications of 𝑃 relativized to 𝐵 [25]. The existence of this more abstract version of forgetting tore open a hole between the semantics and syntax that that was just recently closed [19]. In this paper we were able to close it again by intricately modifying f SP , to be able to take into account a relativization set. Given that most of the recent results are limited to the propositional case, we believe that it would be interesting to explore how they translate to forgetting about predicate-symbols next. This figure illustrates how g R takes a divide and conquer approach to be able to encode the semantics of F rR . Here we abstract away from the specific syntax of each auxiliary program and only look at their models. For each set of models in a box such a representative exists [13]. The models of an initial program 𝑃 are on the top most box, the models of the auxiliary results of forgetting 𝑉 " t𝑞u relativized to 𝐵 " t𝑎, 𝑏, 𝑐u are listed from there on downward. The workings of f rSP follow a similar pattern, but are hard to put into an illustration, since the auxiliary operators g 𝑉,𝐵 W satisfy a lot more models.