On Syntactic Forgetting with relativized Strong Persistence

1. 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 diferent 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 QuineMcCluskey 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 fSP, as its name suggests, satisfies pSPq whenever possible.

Example 1.1. It is possible that by forgetting an atom we

may introduce double negations. E.g. forgetting from “ t Ð ; Ð u results in 1 “ t Ð u

If an atom is forgotten that appears in such a self-loop, the syntactic derivations are a bit opaque. Consider forgetting from the following program:

22nd International Workshop on Nonmonotonic Reasoning, November 2-4, 2024, Hanoi, Vietnam © 2024 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). Ð Ð Ð 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 1There are accessible implementations of all forgetting operators staying within logic programs available online, including the ones in this paper: https://service.scadsai.uni-leipzig.de/ForgettingWeb https://github.com/mattiberthold/ForgettingWeb

2. Background

Given that FrSS and therefore frSP 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 pq Ð B `pq, B ´pq, B ´´pq, where H pq “ t1, . . . , u, B `pq “ t1, . . . , u, B ´pq “ t1, . . . , u, and B ´´pq “ t1, . . . , u, and we will use both forms interchangeably. Given a rule , H pq is called the head of , and B pq “ B `pq Y B ´pq Y B ´´pq is called the body of , where, for a set of atoms, “ t | P u and “ t | P u.

Σp q and Σpq 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 pq Ð B `pq | P such that B ´pq X “

H and B ´´pq Ď 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 |ù , if |ù and |ù , where |ù both denotes the standard satisfaction relation for classical logic and for HT-logic.3 An HT-interpretation x, y is total if “ . Given a rule , x, y |ù , if x, y |ù tu. 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 if 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 if p1q “ p2q and strongly equivalent, 1 ” 2, if p1 Y q “ p2 Y q for any program . It is well-known that 1 ” 2 exactly when ℋ p1q “ ℋ p2q [ 27 ]. Given a set Ď Σ, the -exclusion of a set of answer sets (a set of HT-interpretations) ℳ, denoted ℳ‖ , is tz | P ℳu (txz, 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, 2Although it is possible to define HT-semantics more broadly over (propositional) formulas, here we use a more succinctly definition over logic programs that is closer to the usual definition of answer sets. 3For brevity, parentheses, commas and union signs within HTinterpretations may be omitted, such that, for example, xH, y means xH, Y t, uy. Σ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 if, for each program and each set of atoms , we have: p Yq‖ “ pfp, qYq for all programs with Σpq Ď Σ\ .

Notably, pSPq can be decomposed into the following three properties, i.e. an operator f satisfies pSPq if f satisfies all pwCq, psCq and pSIq, where pwCq f satisfies weakened consequence if, for each and each set of atoms : pfp, qq Ě p q‖ . psCq f satisfies strengthened consequence if, 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 if, for each program and each set of atoms , we have: fp, q Y ” fp Y , q for all programs with Σpq Ď Σ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, if 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 pSPqx, y, if pfp, q Y q “ p Y q‖ , for all programs with Σpq Ď Σ\ . A sound and complete criterion Ω characterizes when it is not possible to forget while satisfying pSPqx, y.

Definition 2.1 (Gonçalves et al. (2016)). Let be a program over Σ and Ď Σ. The forgetting instance x, y satisfies criterion Ω if there exists Ď Σz such that the set of sets ℛx, y :“ t,

x, y | P x, yu is non-empty and has no least element, where x,, y :“ tz | x, Y y P ℋ p qu, and x, y :“ t Ď | x Y , Y y P ℋ p q and

E1 Ă s.t. x Y 1, Y y P ℋ p qu.

Corresponding to the Ω criterion the classes FR and FSP specify the HT-models of the forgetting result. It was shown that FSP satisfies pSPqx, y for all instances x, y that do not satisfy Ω. Moreover, in the case where Ω is satisfied, FSP still exhibits desirable behavior, such as satisfying pSIq and pwCq, two of three characterizing criterions of pSPq. FR 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 FR and FSP are defined as follows: FR :“ tf | ℋ pfp, qq “ tx, y | Ď Σp qz ^ P ď ℛx, yu, for all programs and Ď Σu,

Definition 2.5 (Woltran (2004)). A pair of interpretations x, y is a (relativized) B-HT-interpretation if either “ or Ă p zq. 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 if: 1. |ù ; 2. for all 1 Ă with p 1zq “ p zq : 1 ­|ù ; and 3. Ă implies existence of a 1 Ď with 1z “ , 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 if ℋ p1q “ ℋ p2q.

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.

Definition 2.7 (Saribatur and Woltran (2024)). A forgetting operator f satisfies relativized strong persistence for a relativized forgetting instance x, , y, Ď , denoted by prSPqx,,y, if for all programs over , pfp, , q Y q “ p Y q|| .

As Ω characterizes instances x, y for which pSPq is satisfiable, Ω, characterizes instances x, , y for which prSPqx,,y is satisfiable.

Definition 2.8 (Saribatur and Woltran (2024)). Let be a program over Σ and , Ď Σ. satisfies criterion Ω, if there exists Ď Σz such that the set of sets ℛx,,y :“ ttz | x, Y 1y P ℋ p qu prSPqx,,y, for any Ď .

Proposition 2.9 (Saribatur and Woltran (2024)). If forgetting operator f satisfies pSPqx,y then it satisfies a Definition 2.10 (Saribatur and Woltran (2024)). Given program over Σ and , Ď Σ , the --HT-models of are given by the set ℋ p q :“tx, y|| | x, y P ℋ p qu Y | 1 Ď , x Y 1, Y 1y P ℋ p qu tx, y|| | x, y P ℋ p q, Ă , and for all x 1, 1y P ℋ p q with |1| “ ||, x1, 1y P ℋ p q with 1 “ ||u Definition 2.11 (Saribatur and Woltran (2024)). Let be a program. The relativization of HT-models of over to the set of atoms4 is denoted by ℋ , p q :“ tx, y | x, y P ℋ p q, Ď Σzu. Definition 2.12 (Saribatur and Woltran (2024)).

FrSS :“ tf | ℋ , pfp, , qq “ tx, y | Ď Σz ^ P č ℛx,,yu, for all programs and , Ď Σu

The class FrSS satisfies prSPq whenever possible. Ω, .

Theorem 2.13 (Saribatur and Woltran (2024)). Every f P FrSS satisfies prSPqx,,y, Ď , for every relativized forgetting instance x, , y, where does not satisfy

The following theorem confirms that forgetting can be used as a stepping-stone to, more generally, derive relativized -simplifications.

Theorem 2.14 (Saribatur and Woltran (2024)). Let be -relativized -simplifiable, and f P FrSS. Then fp||X , z, zq is a -relativized -simplification of . 4In order to streamline the presentation the original definition was slightly altered. In particular, ℋ ,p q behaves as if taking into account the complement ¯ of . 2.1. Syntactic Tools Defining a syntactic forgetting operators that obeys the semantics of FrSP inevitably comes down to modifying the existing operator fSP5, 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 ] the program is first brought into a normal form, to avoid complications and unnecessary calculations caused by redundant (parts of) rules.

A rule is tautological if H pq X B `pq ‰ H, B `pq X

B ´pq ‰ H, or B ´pq X B ´´pq ‰ H; is fundamental, if it is not tautological, and H pq X B ´pq “ H and B `pq X B ´´pq “ H.

Definition 2.15 (Cabalar et al. (2007)). and , subsumes , in symbols ď , if:

Given two rules

1. H pq Ď H pq Y B ´pq, 2. B `pq Ď B `pq Y B ´´pq, 3. B ´pq Ď B ´pq, 4. B ´´pq Ď B ´´pq Y B `pq, and 5. B `pq X B ´´pq “ H or H pq X H pq “ H. Proposition 2.16 (Cabalar et al. (2007)).

ď ô ℋ pq Ď ℋ pq

A rule is minimal in , if it is not (strictly) subsumed by another rule in , i.e. if ␣D P : ď ^ ę . Definition 2.17. Let be a program. The normal form p q is obtained from by: 1. removing all tautological rules;

2. removing all atoms from B ´´pq in the remaining

rules , whenever P B `pq;

3. removing all atoms from H pq in the remaining

rules , whenever P B ´pq;

4. removing from the resulting program all rules that are

not minimal.

A program is in normal form if 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 zpq Ð B zpq and z :“ tz | P u.

We define a partition of a program along the occurrences of a given atom .

Definition 2.19 (Berthold (2022)). Given a program in normal form over Σ and an atom P Σ, is partitioned according to the occurrence of , i.e. occp, q :“ x, 0, 1, 2, 3, 4y, where: :“ t P | R Σpqu 0 :“ t P | P pqu 1 :“ t P | P pqu 2 :“ t P | P pq, R pqu 3 :“ t P | P pq, P pqu 4 :“ t P | R pq, P pqu 5By fSP we refer to what is called fS˚P by Berthold (2022).

There are some correspondences between the models of a program and its rules that we can spot by this partitioning. Proposition 2.20 (Berthold (2022)). Given a program in normal form over Σ, Ď Ď Σ, and an atom P Σ, with R , and occp, q “ x, 0, 1, 2, 3, 4y.

Then the following equivalencies hold:

x, y ­|ù ô D P Y 1 Y 4 : x, y ­|ù x, y ­|ù ô D P Y 0 Y 2 : x, y ­|ù x, y ­|ù ô D P Y 2 Y 3 Y 4 : x, y ­|ù The next construction conversely identifies, which interpretations are models of a program.

The as-dual construction [ 17 ] generalizes constructions that collect sets of conjunctions of literals aiming to replace negated occurrences of a literal [ 15, 16 ].

Definition 2.21 (Berthold (2022)). Given a program “ t1, . . . , u over Σ and an atom P Σ, then:

p q :“ tt1, . . . , u |

P B zpq Y H zpq, 1 ď ď u, where, for a set of literals, “ t | P u and “ t | P u, where, for P Σ, we assume the simplification “ and “ .

By applying the as-dual to certain subsets of a program, we are able to construct rules that point towards certain models of a program.

Proposition 2.22 (Berthold (2022)). Given a program in normal form over Σ, Ď Σ, and an atom P Σ, with R , and occp, q “ x, 0, 1, 2, 3, 4y. Then the following implications hold:

x, y |ù ñ D P p1 Y 4q : x, y ­|ù x , y |ù ñ D P p0 Y 2q : x , y ­|ù x, y |ù ñ D P p3 Y 4q : x, y ­|ù Ð

Ð Ð

In the case that “ H the first and second implication hold

in both directions.

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:

H p1q Y H p2q Ð B p1q Y B p2q Proposition 2.24 (Berthold (2022)). Let 1, 2 be rules over Σ, and Ď Ď Σ,

|ù 1 ˆ 2 ô |ù 1 _ |ù 2 |ù t1 ˆ 2u ô |ù t1u _ |ù t2u Definition 2.25 (Product of Programs Berthold (2022)).

Let 1 and 2 be programs. Their product 1 ˆ 2, is

defined as: t1 ˆ 2 | 1 P 1 ^ 2 P 2u Proposition 2.26 (Berthold (2022)). Let 1, 2 be programs over Σ, and Ď Ď Σ,

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

|ù 1 ˆ 2 ô |ù 1 _ |ù 2 |ù p1 ˆ 2q

ô |ù 1 _ |ù 2

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.

Definition 2.27 (Berthold (2022)). Given a rule , we deifne the double negation of , i.e. , as:

:“ Ð H pq Y B pq Proposition 2.28 (Berthold (2022)). Given a rule over Σ, and Ď Ď Σ, the following statement holds: |ù ô x, y |ù

We would like to point out that similarly, a formula holds classically if „„ 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: ℋ p1q Y ℋ p2q “ ℋ pp1 Y 1q ˆ p2 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 diferent 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 ď , if: 1. H pq Ď H pq Y B ´pq, 2. B `pq Ď B `pq, 3. B ´pq Ď B ´pq, and 4. B ´´pq Ď B ´´pq Y B `pq. Then ă , if ď ^ ‰ .

Proposition 2.30. Strong subsumption is finer than regular subsumption: Strong subsumption is anti-symmetric:

ď ñ ď ď ^ ď ñ “ . (1) (2) ă ñ ă ď ^ ď ñ ď .

Strong subsumption is preserved under ˆ:

ď ñ ˆ ď ˆ for all rules .

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

ď ô @ Ď Σ : z ď z.

Proof: ‰ (3) (4) (5) (6) 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 pq X B ´pq “ H “ B `pq X B ´´pq 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 efect on the required subset-relationship. p6q Is a consequence of p5q.

A rule is minimal in , if it is not strongly subsumed by another rule in , i.e. if ␣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.

Proposition 2.31 (Berthold 2022). Given a program in normal form over Σ, Ă Ď Σ, and an atom P Σ, with R , and occp, q “ x, 0, 1, 2, 3, 4y. Then the following hold: x, y ­|ù ô D P 1 Y 4 : x, y ­|ù z _ D P : x, y ­|ù x, y ­|ù ô D P Y 1 Y 4 : x, y ­|ù z x , y ­|ù ô D P 0 Y 2 : x, y ­|ù z _ D P : x, y ­|ù x, y ­|ù ô x , y ­|ù

_ D P 3 Y 4 : x, y ­|ù z x, y |ù ô x , y |ù

^ D P p3 Y 4q : x, y ­|ù Ð x, y ­|ù ô D P Y 0 Y 2 : x, y ­|ù z x, y ­|ù ô x , y ­|ù

If additionally “ H, then

x, y |ù ô D P p1 Y 4q : x, y ­|ù Ð x , y |ù ô D P p0 Y 2q : x, y ­|ù Ð For all 2 P 2: x , y ­|ù 2 ô x, y ­|ù 2, and x, y ­|ù 2 ô x, y ­|ù 2.

The rules identified in Prop. 2.31 constitute the essential pillars of defining forgetting operators.

_ D P Y 2 Y 3 Y 4 : x, y ­|ù z 2.2. Syntactic Forgetting with pSPq Given that the semantics of FrSP and FSP coincide for some inputs, it is not surprising that a representative of FrSP needs to be a modification of fSP. We, hence, recall its construction [ 19 ]. The operator fSP is defined via two auxiliary operators fR and fW, each of which is again defined using auxiliary operators fR and fW, which are defined inductively.

Definition 2.32 ( fR`). Given a program in normal form

over Σ and P Σ s.t. occp, q “ x, 0, 1, 2, 3, 4y. Then:

fR`p, q :“ p1 Y 2 Y 3 Y 4q where: asd

1 :“ tÐ | P p3 Y 4qu 2 :“ t z | P 0 Y 2u 3 :“ tz | P Y 2u 4 :“ tp0 ˆ 1qz | 0 P 0, 1 P 3 Y 4u

Proposition 2.33. Given a program over Σ, an atom P

Σ, and sets and , s.t. Ă Ď Σztu, then: x, y |ù fR`p, q ô tu P x,tuy If tu P x,tuy, then: x, y |ù fR`p, q ô x, y |ù _ x, y |ù

Definition 2.34 ( fR´). Given a program in normal form

over Σ and P Σ s.t. occp, q “ x, 0, 1, 2, 3, 4y.

Then:

The operators fR is defined inductively by nested calls on fR` and fR´. In order to fix a concrete forgetting result, we assume an arbitrary order on , which has no efect on the following propositions.

Definition 2.35 ( fR). Let be a program over Σ, and

Ď t1, 2, . . . , u “ Ď Σ, s.t. 0 ă , then: fRp, Hq :“ fRp, q :“ fRb pfRz p, ztuq, q

fRp, q :“ p ą fp, qq

Ď Theorem 2.38. fR P FR fSP. 1 :“ t1z ˆ Ð | 1 P Y 1 Y 4, P p1 Y 4qu

Definition 2.41 ( fW). Let be a program over Σ, and

Ď t1, 2, . . . , u “ Ď Σ, s.t. 0 ă , then: fWp, Hq :“ fWp, q :“ fWb pfWz p z, ztuq, q Y fb :“ W #f`, if P

W f´, otherwise

W :“ t P | X Σpq “ Hu

Proposition 2.42. Given a program over Σ, and sets ,

, and , s.t. Ď Ď Σ, Ď Ď Σz , and “ t P | X Σpq “ Hu “ H, then: P x, y ^ @2 Ď : x2, y ­|ù ô x, y ­|ù fWp, q

Definition 2.43 ( fW). Given a program in normal form

over Σ and Ď Σ. Then: fWp, q :“ p ď fWp, qq Ď

Definition 2.44 ( fS˚P). Let be a program over Σ in normal

form and Ď Σ.

fSPp, q :“ pfWp, q Y fRp, qq Example 2.45. Let 2.45 “ t Ð , ; Ð , ; Ð u, and “ t, u. Then fSPp, q can be derived by: ftup, q Ď t Ð u R ftup, q “ t Ð , u

W fRHp, q Ď t Ð u

fWHp, q “ t Ð , u fSPp, q “ pfRtup, q ˆ fRHp, q

Y ftup, q Y fWHp, qq

W “ t _ Ð , ; Ð , ; Ð , u Theorem 2.46. fSP P FSP 3. 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 fSP is a member of another class FR. We define a relaxation FrR of this class too, to aim for first.

FrR :“ tf | ℋ , pfp, , qq “ tx, y | Ď Σz ^ P ď ℛx,,yu, for all programs and , Ď Σu While the ‘r’ in prSPq and the ‘R’ in FR both mean ‘relativized’, it is not clear in which sense FR corresponds to the idea of relativized equivalence. Still we use the subscript ‘rR’ for this new class in reference to its origin in FR.

Assume a program over Σ, , Ď Σ, s.t. X “ H, and Ď . If we take a look at the definition of the class FrR, we can note that there is a similarity in how it treats forgotten atoms and atoms that it relativizes from Σp qz: • Given Ď , a total model x , y of , s.t. there is a 1 Ď with x 1, y |ù is not considered by ℛx,,y; • Similarly, given Ď Σp qzp Y q, a total model x , y of , s.t. there is a 1 Ď with x 1, y |ù is not considered by ℛx,,y, by the construction of ℋ p q.

The operator fR includes an encoding for the first bulletpoint. The key-idea therefore is to manipulate the auxiliary constructions of fR further, to encode the second bulletpoint.

For each Ď and Ď Σp qzp Y q, we deifne an auxiliary operator gR, 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 11, y |ù . Then gR, p, q, satisfies x , y, if (i) and (ii). Further, we let g, p, q contradict each x2, y with Ă ,

R 2 Ď , if ­|ù x 11, y for all 1 Ă and 1 Ă .

The operators g, are defined taking into account fR as

R a baseline, i.e. g, p, , q :“ gR pfRp, q, q. These

R gR we define inductively, starting at || “ 1.

Definition 3.1 ( gR`). Given a program in normal form

over Σ and P Σ s.t. occp, q “ x, 0, 1, 2, 3, 4y. Then:

gR`p, q :“ p1 Y 2 Y 3 Y 4 Y 5q gR p, q :“ gRb pgRz p, ztuq, q 4. Syntactic Forgetting with prSPq Again we define gW s.t. it modifies an auxiliary result of fW to take into account whether a Ď ¯ :“ Σp qz is relevant.

Remember, that the auxiliary operators fW implement a check for whether is relevant for ( P x, y), i.e. that x , y is a model of , but x 1, y is not a model of for all 1 Ă . As we have seen in the last section this requirement extends to relativized forgetting, in the sense that we additionally need to check whether Y can be a stable model of under addition of rules over – gW checks, whether x , y |ù and x 1, y ­|ù for all 1 Ă .

By compounding the constructions f with gW , i.e. W g, p, , q :“ gW pfWp, q, q, we get operators with W the following properties.

Given a program over Σ, , Ď Σ with X “ H, Ď Ď Σ X , Ď , and 1 Ď Ď Σp qz, then, g, p, , q contradicts x1, y i.e. x1, y ­|ù W g, p, , q, if x , y |ù , for all 1 Ď and W 2 Ď with 1 Y 2 Ă Y : x 12, y ­|ù , and for all 1 Ď : x11, y ­|ù .

The auxiliary operators gW are again inductively defined via gW` and g´ .

W Definition 4.1 ( gW`). Given a program in normal form over Σ and P Σ s.t. occp, q “ x, 0, 1, 2, 3, 4y, then:

gW`p, q :“ p1 Y 2q The building-blocks gW` and gW´ of our inductive definition take into account one atom that is relativized away. We can therefore again use the observations of Prop. 2.31 to see that for the case || “ 1 they have the desired properties.

Proposition 4.2. Given a program over Σ, an atom P Σ, and sets and , s.t. Ă Ď Σ, then:

x, y ­|ù gR`p, q ô |ù ^ P ^ ztu ­|ù ^ x, y ­|ù Definition 4.3 ( gW´). Given a program in normal form over Σ and P Σ s.t. occp, q “ x, 0, 1, 2, 3, 4y, then:

gW´p, q :“ p1q

Proposition 4.4. Given a program over Σ, an atom P Σ, and sets and , s.t. Ă Ď Σ, then:

x, y ­|ù gR´p, q ô R ^ |ù ^ x, y ­|ù

To define gW for arbitrary Ď Σp qz, we assume an arbitrary ordering on Σ, e.g. the lexicographic order, and apply repeatedly the operators gW` or g´ , depending W on whether an atom is in . For example, let be over t, , , u, “ t, u and “ tu, then gW p, q “ gW`pgW´p, q, q.

Definition 4.5 ( gW ). Let be a program over Σ, Ď Σ and Ď t1, 2, . . . , u “ ¯ :“ Σp qz, s.t. 0 ă , then: gW p, Hq :“ gW p, q :“ gWb pgWz p z, ¯ztuq, q Y where: gb :“ W #g` , if P

W g´ , otherwise

W :“ t P | Σpq Ď u

The fact that the properties of gW` and gW´ extend to gW can be checked rather straight-forwardly by induction. Proposition 4.6. Given a program over Σ, sets of atoms Ď Σ, Ď Σp qz, and sets and , s.t. Ă Ď Σ, then:

x, y ­|ù gW p, q ô |ù ^ z “ ^ E 1 Ă , s.t. 1 |ù and 1 X “ X ^ x, y ­|ù

To construct gW, fW and gW are compounded for each Ď and Ď Σp qz, i.e. gW, p, , q :“ gW pfWp, q, q. The resulting rules of each of these compounds are then united.

Definition 4.7 ( gW). Given a program in normal form over Σ and Ď Σ. Then: gWp, , q :“ p ď gW, p, , qq

frSPp, q :“ pgWp, q Y gRp, qq Theorem 4.9. frSP P FrSS

Corollary 4.10. Let be -relativized -simplifiable, then

frSPp||X , z, q is a -relativized -simplification of . 5. 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, pq, p q. pq Ð p, q. p q Ð p, q.

A possible forgetting result in full first order syntax is : @, : p␣D : pp, q ^ p, qq ^ pq ^ p q Ñ p, q ^ p, q Ñ ppq ^ pqqq 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 ].

6. Conclusion

The question on how a logic program may be simplified, has become a rather large one, sparking several subtopics that cover diferent 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 fSP, 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. gRtℎupfRHp, q, q

gRHpfRHp, q, q gRp, , q

Acknowledgements

This work was supported by the German Federal Ministry of Education and Research (BMBF, 01IS18026B-F) by funding the competence center for Big Data and AI “ScaDS.AI” Dresden/Leipzig.

References

[1] A. Heyting , Die formalen regeln der intuitionistischen logik, in: Sitzungsberichte der Preussischen Akademie der Wissenschaften . Physikalischmathematische Klasse , 1930 .

[2] V. Lifschitz , D. Pearce , A. Valverde , A characterization of strong equivalence for logic programs with variables , in: Proceedings of (LPNMR-07) , 2007 . doi: 10 . 1007/978-3- 540 -72200-7\_ 17 .

[3] Y. Chen , Y. Zhang , Y. Zhou , First-order indefinability of answer set programs on finite structures , in: Proceedings of (AAAI-10) , 2010 .

[4] F. Lin , R. Reiter , Forget it, in: Working Notes of AAAI Fall Symposium on Relevance , 1994 .

[5] J. P. Delgrande , A knowledge level account of forgetting , Journal of Artificial Intelligence Research ( 2017 ). doi: 10 .1613/jair.5530.

[6] T. Eiter , G. Kern-Isberner , A brief survey on forgetting from a knowledge representation and reasoning perspective , KI - Künstliche Intelligenz ( 2018 ). doi:10.1007/s13218-018-0564-6.

[7] R. Gonçalves , M. Knorr , J. Leite, The ultimate guide to forgetting in answer set programming , in: Proceedings of (KR-16) , 2016 .

[8] R. Gonçalves , M. Knorr , J. Leite , You can't always forget what you want: On the limits of forgetting in answer set programming , in: Proceedings of (ECAI-16) , 2016 . doi: 10 .3233/978-1- 61499 -672-9-957.

[9] R. Gonçalves , M. Knorr , J. Leite , S. Woltran , When you must forget: Beyond strong persistence when forgetting in answer set programming , Theory and Practice of Logic Programming ( 2017 ).

[10] R. Gonçalves , T. Janhunen , M. Knorr , J. Leite , S. Woltran , Forgetting in modular answer set programming , in: Proceedings of (AAAI-19) , 2019 . doi: 10 . 1609/aaai.v33i01. 33012843 .

[11] R. Gonçalves , T. Janhunen , M. Knorr , J. Leite , On syntactic forgetting under uniform equivalence , in: Proceedings of (JELIA-21) , volume 12678 , 2021 , pp. 297 - 312 . doi: 10 .1007/978-3- 030 -75775-5\_ 20 .

[12] P. Cabalar , P. Ferraris , Propositional theories are strongly equivalent to logic programs , Theory and Practice of Logic Programming ( 2007 ).

[13] P. Cabalar , D. Pearce , A. Valverde , Minimal logic programs , in: Proceedings of (ICLP-07) , 2007 .

[14] Y. Zhang , N. Y. Foo , Solving logic program conflict through strong and weak forgettings , Artificial Intelligence 170 ( 2006 ) 739 - 778 . doi: 10 .1016/j.artint. 2006 . 02 .002.

[15] T. Eiter , K. Wang , Semantic forgetting in answer set programming , Artificial Intelligence ( 2008 ).

[16] M. Knorr , J. J. Alferes , Preserving strong equivalence while forgetting , in: Proceedings of (JELIA-14) , 2014 . doi: 10 .1007/978-3- 319 -11558-0_ 29 .

[17] M. Berthold , R. Gonçalves , M. Knorr , J. Leite , A syntactic operator for forgetting that satisfies strong persistence , Theory and Practice of Logic Programming ( 2019 ). doi: 10 .1017/S1471068419000346.

[18] R. Gonçalves , T. Janhunen , M. Knorr , J. Leite , On syntactic forgetting under uniform equivalence , in: Proceedings of (JELIA-21) , 2021 . doi: 10 .1007/ 978-3- 030 -75775-5\_ 20 .

[19] M. Berthold , On syntactic forgetting with strong persistence , in: Proceedings of (KR-22) , 2022 .

[20] F. Aguado , P. Cabalar , J. Fandinno , D. Pearce , G. Pérez, C. Vidal , Syntactic ASP forgetting with forks , Artificial Intelligence ( 2024 ). doi: 10 .1016/J.ARTINT. 2023 . 104033 .

[21] Z. G. Saribatur , T. Eiter, Omission-based abstraction for answer set programs , in: Proceedings of (KR-18) , 2018 .

[22] T. Eiter , Z. G. Saribatur , P. Schüller , Abstraction for zooming-in to unsolvability reasons of grid-cell problems , CoRR ( 2019 ). arXiv: 1909 .04998.

[23] Z. G. Saribatur , T. Eiter , A semantic perspective on omission abstraction in ASP , in: Proceedings of (KR20) , 2020 . doi: 10 .24963/KR. 2020 /75.

[24] Z. G. Saribatur , S. Woltran , Foundations for projecting away the irrelevant in ASP programs , in: Proceedings of (KR-23) , 2023 . doi: 10 .24963/KR. 2023 /60.

[25] Z. G. Saribatur , S. Woltran , A unified view on forgetting and strong equivalence notions in answer set programming , in: Proceedings of (AAAI-24) , 2024 . doi: 10 .1609/AAAI.V38I9.28940.

[26] V. Lifschitz , L. R. Tang , H. Turner , Nested expressions in logic programs , Annals of Mathematics and Artificial Intelligence ( 1999 ). doi: 10 .1023/A: 1018978005636 .

[27] V. Lifschitz , D. Pearce , A. Valverde , Strongly equivalent logic programs , ACM Transactions on Computational Logic ( 2001 ).

[28] S. Woltran , Characterizations for relativized notions of equivalence in answer set programming , in: Proceedings of (JELIA-04) , 2004 . doi: 10 .1007/ 978-3- 540 -30227-8\_ 16 .

[29] K. Inoue , C. Sakama , Negation as failure in the head , Journal of Logic Programming ( 1998 ).

[30] K. Inoue , C. Sakama , Equivalence of logic programs under updates , in: Proceedings of (JELIA-04) , 2004 .

[31] M. Slota , J. Leite , Back and forth between rules and SE-models , in: Proceedings of (LPNMR-11) , 2011 .

[32] Y. Zhou , Y. Zhang, Bounded forgetting , in: Proceedings of (AAAI-11) , 2011 . doi: 10 .1609/AAAI.V25I1. 7842.

[33] B. Bogaerts , T. Janhunen , S. Tasharrofi , Stable-unstable semantics: Beyond NP with normal logic programs , Theory and Practice of Logic Programming ( 2016 ). doi: 10 .1017/S1471068416000387.

[34] G. Amendola , F. Ricca , M. Truszczynski , Beyond NP : quantifying over answer sets , Theory and Practice of Logic Programming ( 2019 ). doi: 10 .1017/ S1471068419000140.

[35] J. Heuer , C. Wernhard , Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via craig interpolation in first-order logic , CoRR ( 2024 ). doi: 10 .48550/ARXIV.2402. 07696. arXiv: 2402 . 07696 .