=Paper=
{{Paper
|id=Vol-3835/paper18
|storemode=property
|title=On Syntactic Forgetting with relativized Strong Persistence
|pdfUrl=https://ceur-ws.org/Vol-3835/paper18.pdf
|volume=Vol-3835
|authors=Matti Berthold
|dblpUrl=https://dblp.org/rec/conf/nmr/Berthold24
}}
==On Syntactic Forgetting with relativized Strong Persistence==
https://ceur-ws.org/Vol-3835/paper18.pdf
On Syntactic Forgetting with relativized Strong Persistence
Matti Berthold
ScaDS.AI, Universität Leipzig
Abstract
Strong Persistence pSPq, since its perception ten years ago, has been at the center of attention in the realm of forgetting in logic
programming. So-called forgetting instances, for which it is possible to obtain pSPq were characterized; semantic classes of procedures
satisfying pSPq when possible, or various relaxations when it is not, were found; and concrete operators representing these classes
were constructed. Recently, pSPq was relaxed in a novel dimension, taking into account the strong persistence of a forgetting result
relativized to a subset of the remaining atoms. In this paper, we construct a syntactic forgetting operator that satisfies this newly defined
desideratum relativized Strong Persistence prSPq, whenever possible.
1. Introduction
Logic programming (LP) under answer set semantics is a 𝑎Ð𝑞 𝑏 Ð 𝑛𝑜𝑡 𝑞 𝑞 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞
declarative non-monotonic reasoning formalism with a ro- Already, it is impossible to satisfy pSPq [8]. However, a possi-
bust theoretical (and monotonic) foundation based in in- ble result satisfying a relaxation of pSPq may be [17]:
tuitionistic 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 expres- where 𝑎 and 𝑏 each support themselves, and at least one of
sive power than first-order logic, making it possible, for them is true.
example, to identify Hamiltonian cycles [3]. The fact that forgetting in practice should not be done by
The question of how a program may be simplified is not hand, is probably best witnessed by the fact that forgetting
simply answered. The surge of research around it, rather about multiple atoms may not be reduced to forgetting them in
suggests that it is very nuanced, where the limits and pos- iteration. Rather, the result is derived by a recursive derivation
sibilities vary greatly, depending on the exact definition of tree [19]. 1
what is meant by being simpler, and the concrete formal- Abstraction by omission [21, 22, 23] can be seen as a re-
ism that is being investigated. Such processes might find laxed version of forgetting, where atoms are removed from
application, e.g. in a legal context; in order to exclude de- a program, but its answer-sets are only required to behave
pendencies that are no longer deemed relevant; or to reduce as before, under no addition of another program 𝑅.
the complexity of reasoning tasks. The aptly named Simplification [24] reduces the signature
Forgetting [4, 5, 6], or variable elimination, which is one of a program 𝑃 by a set of atoms 𝐴 as well, requiring the
such possible interpretation of simplification, intuitively result to behave the same as 𝑃 under a context program 𝑅
means that a programs signature is restricted, while the log- that may contain atoms 𝐴 in a restricted way.
ical dependencies of the remaining atoms are left unchanged. These different ideas as well as several versions of equiv-
It has been considered with respect to many properties in- alence were recently captured by an overarching notion of
cluding strong persistence pSPq which seemingly captures 𝐴-simplifications of 𝑃 relative to 𝐵, where 𝐴 is a set of atoms
best its intuitions [7]. In essence, pSPq ensures that the that is to be removed, and 𝐵 is the signature of possible con-
result of forgetting atoms 𝑉 from a program 𝑃 exerts the text programs 𝑅 [25]. Interestingly, by taking into account
same behavior as 𝑃 under the addition of a context program the full spectrum of all of these ideas, a novel, relaxed ver-
𝑅 not containing any forgotten atoms. There are instances sion of pSPq, so-called relativized Strong Persistence prSPq
for which pSPq is impossible to be achieved [8]. Follow- emerged.
ing this negative result, several relaxations of pSPq were What is missing from the picture now, is a concrete syn-
proposed, which are attainable through different semantic tactic transformation frSP that satisfies prSPq, whenever
means [9, 10, 11]. possible. Since pSPq and prSPq coincide in some cases, it is
While results of forgetting using the desired seman- clear that we should start our search at fSP and see how we
tics may be obtained by counter-model construction [12] get to frSP from there. While the question this paper is out
and perhaps be minimized using a version of the Quine- to answer may appear simple at first, its answer is far from
McCluskey algorithm [13], a much more direct and conser- it. To be able to construct frSP , it turns out that it is neces-
vative approach is to forget by syntactically manipulating an sary to intrically modify sub-procedures of fSP . Finally, with
input program. There are several such syntactical operators this operator at our disposal, we are then able to construct
in the literature [14, 15, 16, 17, 18, 19, 20], where notably syntactically general 𝐵-relativized 𝐴-simplifications.
fSP , as its name suggests, satisfies pSPq whenever possible. Given that the class of forgetting operators FrSS to satisfy
prSPq, whenever possible, is defined methodologically to
Example 1.1. It is possible that by forgetting an atom we
meet this criterion, and that the operator frSP is defined
may introduce double negations. E.g. forgetting 𝑞 from 𝑃 “
methodologically to match FrSS , we assume any intuition
t𝑎 Ð 𝑛𝑜𝑡 𝑞; 𝑞 Ð 𝑛𝑜𝑡 𝑎u results in 𝑃 1 “ t𝑎 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎u
about the derivation rules one may find to be ‘post hoc’. We
If an atom is forgotten that appears in such a self-loop, the
therefore leave the task of finding an intuitive explanation
syntactic derivations are a bit opaque. Consider forgetting 𝑞
of why they are as they are for future studies.
from the following program:
1
There are accessible implementations of all forgetting operators staying
22nd International Workshop on Nonmonotonic Reasoning, November 2-4, within logic programs available online, including the ones in this paper:
2024, Hanoi, Vietnam https://service.scadsai.uni-leipzig.de/ForgettingWeb
© 2024 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0
International (CC BY 4.0). https://github.com/mattiberthold/ForgettingWeb
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
2. Background Σpfp𝑃, 𝑉 qq Ď Σp𝑃 qz𝑉 is usually required. In the follow-
ing we introduce some well-known properties for forgetting
Given that FrSS and therefore frSP require the understanding operators [8].
of several topics that are ‘non-canon’ and scientific papers Strong persistence is presumably the best known one [16].
should be self-contained there is a surprising amount of It requires that the result of forgetting fp𝑃, 𝑉 q is strongly
research to be recalled, in spite of the fact that the topic of equivalent to the original program 𝑃 , modulo the forgotten
this paper is forgetting. Therefore, after recalling the foun- atoms.
dations of logic programming, we compile and streamline a
rather long list of definitions and results from the literature. pSPq f satisfies strong persistence iff, for each program 𝑃
and each set of atoms 𝑉 , we have:
Logic Programs. We assume a propositional signature Σ. 𝒜𝒮p𝑃 Y𝑅q‖𝑉 “ 𝒜𝒮pfp𝑃, 𝑉 qY𝑅q for all programs
A logic program 𝑃 over Σ is a finite set of rules of the form 𝑅 with Σp𝑅q Ď Σ\𝑉 .
Notably, pSPq can be decomposed into the following three
𝑎1 _ . . . _ 𝑎𝑘 Ð 𝑏1 , . . . , 𝑏𝑙 , 𝑛𝑜𝑡 𝑐1 , . . . , 𝑛𝑜𝑡 𝑐𝑚 ,
properties, i.e. an operator f satisfies pSPq iff f satisfies all
𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑1 , . . . , 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑𝑛 , pwCq, psCq and pSIq, where
where all 𝑎1 , . . . , 𝑎𝑘 , 𝑏1 , . . . , 𝑏𝑙 , 𝑐1 , . . . , 𝑐𝑚 , and 𝑑1 , . . . , 𝑑𝑛 pwCq f satisfies weakened consequence iff, for each 𝑃 and
are atoms of Σ [26]. Such rules 𝑟 are also written more each set of atoms 𝑉 : 𝒜𝒮pfp𝑃, 𝑉 qq Ě 𝒜𝒮p𝑃 q‖𝑉 .
succinctly as psCq f satisfies strengthened consequence iff, for each
𝑃 and each set of atoms 𝑉 : 𝒜𝒮pfp𝑃, 𝑉 qq Ď
H p𝑟q Ð B ` p𝑟q, 𝑛𝑜𝑡 B ´ p𝑟q, 𝑛𝑜𝑡 𝑛𝑜𝑡 B ´´ p𝑟q, 𝒜𝒮p𝑃 q‖𝑉 .
where H p𝑟q “ t𝑎1 , . . . , 𝑎𝑘 u, B ` p𝑟q “ t𝑏1 , . . . , 𝑏𝑙 u, Strong invariance requires that rules not mentioning atoms
B ´ p𝑟q “ t𝑐1 , . . . , 𝑐𝑚 u, and B ´´ p𝑟q “ t𝑑1 , . . . , 𝑑𝑛 u, to be forgotten can be added before or after forgetting.
and we will use both forms interchangeably. Given a rule
pSIq f satisfies strong invariance iff, for each program 𝑃
𝑟, H p𝑟q is called the head of 𝑟, and B p𝑟q “ B ` p𝑟q Y
and each set of atoms 𝑉 , we have: fp𝑃, 𝑉 q Y 𝑅 ”
𝑛𝑜𝑡 B ´ p𝑟qY𝑛𝑜𝑡 𝑛𝑜𝑡 B ´´ p𝑟q is called the body of 𝑟, where,
fp𝑃 Y 𝑅, 𝑉 q for all programs 𝑅 with Σp𝑅q Ď Σz𝑉 .
for a set 𝐴 of atoms, 𝑛𝑜𝑡 𝐴 “ t𝑛𝑜𝑡 𝑞 | 𝑞 P 𝐴u and
𝑛𝑜𝑡 𝑛𝑜𝑡 𝐴 “ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞 | 𝑞 P 𝐴u. Note that the presented properties are often considered
Σp𝑃 q and Σp𝑟q denote the set of atoms appearing in 𝑃 for certain subclasses such as disjunctive, normal or Horn
and 𝑟, respectively. programs. Moreover, they naturally extend over classes of
Given a program 𝑃 and an interpretation, i.e., a set forgetting operators, where a class satisfies a property, iff
𝐼 Ď Σ of atoms, the reduct of 𝑃 given 𝐼, is defined as all its members do.
𝑃 𝐼 “ tH p𝑟q Ð B ` p𝑟q | 𝑟 P 𝑃 such that B ´ p𝑟q X 𝐼 “ In the light of the impossibility for a forgetting operator to
H and B ´´ p𝑟q Ď 𝐼u. An HT-interpretation is a pair x𝑋, 𝑌 y satisfy pSPq for all pairs x𝑃, 𝑉 y, called forgetting instances,
s.t. 𝑋 Ď 𝑌 Ď Σ. Given a program 𝑃 , an HT-interpretation where 𝑃 is a program and 𝑉 is a set of atoms to be forgot-
x𝑋, 𝑌 y is an HT-model2 of 𝑃 , x𝑋, 𝑌 y |ù 𝑃 , iff 𝑌 |ù 𝑃 ten from 𝑃 [8], pSPq was defined for concrete forgetting
and 𝑋 |ù 𝑃 𝑌 , where |ù both denotes the standard sat- instances. A forgetting operator f satisfies pSPqx𝑃,𝑉 y , if
isfaction relation for classical logic and for HT-logic.3 An 𝒜𝒮pfp𝑃, 𝑉 q Y 𝑅q “ 𝒜𝒮p𝑃 Y 𝑅q‖𝑉 , for all programs 𝑅
HT-interpretation x𝑋, 𝑌 y is total iff 𝑋 “ 𝑌 . Given a rule with Σp𝑅q Ď Σ\𝑉 . A sound and complete criterion Ω char-
𝑟, x𝑋, 𝑌 y |ù 𝑟, iff x𝑋, 𝑌 y |ù t𝑟u. We admit that the acterizes when it is not possible to forget while satisfying
set of HT-models of a program 𝑃 is restricted to Σp𝑃 q pSPqx𝑃,𝑉 y .
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 Definition 2.1 (Gonçalves et al. (2016)). Let 𝑃 be a pro-
𝑃 iff x𝑌, 𝑌 y P ℋ𝒯 p𝑃 q, and there is no 𝑋 Ă 𝑌 such gram over Σ and 𝑉 Ď Σ. The forgetting instance x𝑃, 𝑉 y
that x𝑋, 𝑌 y P ℋ𝒯 p𝑃 q. We term HT-models x𝑋, 𝑌 y s.t. satisfies criterion Ω if there exists 𝑌 Ď Σz𝑉 such that the set
𝑋 Ă 𝑌 witnesses. The set of all answer sets of 𝑃 is de- of sets ℛ𝑌x𝑃,𝑉 y :“ t𝑅x𝑃,𝑉𝑌,𝐴 𝑌
y | 𝐴 P 𝑅𝑒𝑙x𝑃,𝑉 y u is non-empty
noted by 𝒜𝒮p𝑃 q. Two programs 𝑃1 , 𝑃2 are equivalent iff and has no least element, where
𝒜𝒮p𝑃1 q “ 𝒜𝒮p𝑃2 q and strongly equivalent, 𝑃1 ” 𝑃2 , 𝑌,𝐴
iff 𝒜𝒮p𝑃1 Y 𝑅q “ 𝒜𝒮p𝑃2 Y 𝑅q for any program 𝑅. It 𝑅x𝑃,𝑉 y :“ t𝑋z𝑉 | x𝑋, 𝑌 Y 𝐴y P ℋ𝒯 p𝑃 qu, and
is well-known that 𝑃1 ” 𝑃2 exactly when ℋ𝒯 p𝑃1 q “ 𝑌
𝑅𝑒𝑙x𝑃,𝑉 y :“ t𝐴 Ď 𝑉 | x𝑌 Y 𝐴, 𝑌 Y 𝐴y P ℋ𝒯 p𝑃 q and
ℋ𝒯 p𝑃2 q [27]. Given a set 𝑉 Ď Σ, the 𝑉 -exclusion of a set of
answer sets (a set of HT-interpretations) ℳ, denoted ℳ‖𝑉 , E𝐴1 Ă 𝐴 s.t. x𝑌 Y 𝐴1 , 𝑌 Y 𝐴y P ℋ𝒯 p𝑃 qu.
is t𝑋z𝑉 | 𝑋 P ℳu (tx𝑋z𝑉, 𝑌 z𝑉 y | x𝑋, 𝑌 y P ℳu).
Corresponding to the Ω criterion the classes FR and FSP
specify the HT-models of the forgetting result. It was shown
Forgetting: Properties and Operators. Let 𝒫 be the that FSP satisfies pSPqx𝑃,𝑉 y for all instances x𝑃, 𝑉 y that
set of all logic programs. A forgetting operator is a (partial) do not satisfy Ω. Moreover, in the case where Ω is satisfied,
function f : 𝒫 ˆ 2Σ Ñ 𝒫. The program fp𝑃, 𝑉 q is inter- FSP still exhibits desirable behavior, such as satisfying pSIq
preted as the result of forgetting about 𝑉 from 𝑃 . Moreover, and pwCq, two of three characterizing criterions of pSPq.
2
FR on the other hand always satisfies psCq and pSIq, which
Although it is possible to define HT-semantics more broadly over
makes it an ideal choice, if no new answer sets should be
(propositional) formulas, here we use a more succinctly definition over
logic programs that is closer to the usual definition of answer sets. created [9].
3
For brevity, parentheses, commas and union signs within HT- The classes FR and FSP are defined as follows:
interpretations may be omitted, such that, for example, xH, 𝑌 𝑝𝑞y
means xH, 𝑌 Y t𝑝, 𝑞uy. FR :“ tf | ℋ𝒯 pfp𝑃, 𝑉 qq “ tx𝑋, 𝑌 y | 𝑌 Ď Σp𝑃 qz𝑉 ^
ď
𝑋P ℛ𝑌x𝑃,𝑉 y u, for all programs 𝑃 and 𝑉 Ď Σu, The relativized equivalence can similarly be taken into
account in forgetting.
FSP :“ tf | ℋ𝒯 pfp𝑃, 𝑉 qq “ tx𝑋, 𝑌 y | 𝑌 Ď Σp𝑃 qz𝑉 ^
č 𝑌
𝑋P ℛx𝑃,𝑉 y u, for all programs 𝑃 and 𝑉 Ď Σu. Definition 2.7 (Saribatur and Woltran (2024)). A
forgetting operator f satisfies relativized strong persistence
Abstraction and Simplification. Abstraction as an over- for a relativized forgetting instance x𝑃, 𝑉, 𝐵y, 𝑆 Ď 𝐴,
approximation is defined as follows. denoted by prSPqx𝑃,𝑉,𝐵y , if for all programs 𝑅 over 𝐵,
𝒜𝒮pfp𝑃, 𝑉, 𝐵q Y 𝑅q “ 𝒜𝒮p𝑃 Y 𝑅q||𝑉 .
Definition 2.2 (Saribatur and Eiter (2018)). Given 𝑃
over Σ and 𝑄 over Σ1 with |Σ| ě |Σ1 |, and a mapping As Ω characterizes instances x𝑃, 𝑉 y for which pSPq
𝑚 : Σ Ñ Σ1 Y tJu, 𝑄 is an abstraction of 𝑃 w.r.t. 𝑚, if is satisfiable, Ω𝐴,𝐵 characterizes instances x𝑃, 𝐴, 𝐵y for
𝑚p𝒜𝒮p𝑃 qq Ď 𝒜𝒮p𝑄q. which prSPqx𝑃,𝐴,𝐵y is satisfiable.
For an omission abstraction, i.e. Σ1 Ď Σ, this becomes Definition 2.8 (Saribatur and Woltran (2024)). Let 𝑃
pwCq. An abstraction is called faithful, if it additionally be a program over Σ and 𝐴, 𝐵 Ď Σ. 𝑃 satisfies criterion
satisfies psCq. Ω𝐴,𝐵 if there exists 𝑌 Ď Σz𝐴 such that the set of sets
This notion was later generalized to take into account
context programs, of a certain form, where a program 𝑅 ℛ𝑌x𝑃,𝐴,𝐵y :“ tt𝑋z𝐴 | x𝑋, 𝑌 Y 𝐴1 y P ℋ𝒯 𝐵 p𝑃 qu
over Σ is 𝐴-separated, if there are 𝑅1 over Σz𝐴 and 𝑅2
| 𝐴1 Ď 𝐴, x𝑌 Y 𝐴1 , 𝑌 Y 𝐴1 y P ℋ𝒯 𝐵 p𝑃 qu
over 𝐴, s.t. 𝑅 “ 𝑅1 Y 𝑅2 .
Definition 2.3 (Saribatur and Woltran (2023)). Given, Proposition 2.9 (Saribatur and Woltran (2024)). If a
𝑃 over Σ, 𝐴 Ď Σ, and 𝑄 over Σz𝐴. Q is a strong forgetting operator f satisfies pSPqx𝑃,𝐴y then it satisfies
𝐴-simplification of 𝑃 if for any program 𝑅 over Σ that is prSPqx𝑃,𝐴,𝐵y , for any 𝐵 Ď 𝐴.
𝐴-separated:
Definition 2.10 (Saribatur and Woltran (2024)). Given
𝒜𝒮p𝑃 Y 𝑅q||𝐴 “ 𝒜𝒮p𝑄 Y 𝑅||𝐴 q program 𝑃 over Σ and 𝐴, 𝐵 Ď Σ , the 𝐴-𝐵-HT-models of
𝑃 are given by the set
where:
𝑅||𝐴 :“ tH p𝑟q Ð B p𝑟qzp𝐴 Y 𝑛𝑜𝑡 𝑛𝑜𝑡 𝐴q | ℋ𝒯 𝐵 𝐵
𝐴 p𝑃 q :“tx𝑌, 𝑌 y||𝐴 | x𝑌, 𝑌 y P ℋ𝒯 p𝑃 qu Y
pH p𝑟q Y B ` p𝑟qq X 𝐴 “ Hq, 𝑟 P 𝑅u tx𝑋, 𝑌 y||𝐴 | x𝑋, 𝑌 y P ℋ𝒯 𝐵 p𝑃 q, 𝑋 Ă 𝑌,
𝑃 is strong 𝐴-simplifiable if there is such a 𝑄. and for all x𝑌 1 , 𝑌 1 y P ℋ𝒯 𝐵 p𝑃 q with 𝑌||𝐴
1
“ 𝑌||𝐴 ,
x𝑋 1 , 𝑌 1 y P ℋ𝒯 𝐵 p𝑃 q with 𝑋 1 “ 𝑋||𝐴 u
Theorem 2.4 (Saribatur and Woltran (2023)). If pro-
gram 𝑃 is strongly 𝐴-simplifiable, then 𝑃||𝐴 is a strong Definition 2.11 (Saribatur and Woltran (2024)). Let 𝑃
𝐴-simplification of 𝑃 . be a program. The relativization of HT-models of 𝑃 over 𝐴
to the set 𝐵 of atoms4 is denoted by
Relativized (Strong) Simplification. Recently simplifi-
cations have been relaxed to take into account relativized ℋ𝒯 𝐴,𝐵 p𝑃 q :“ tx𝑋, 𝑌 y | x𝑋, 𝑌 y P ℋ𝒯 𝐵 p𝑃 q, 𝑌 Ď Σz𝐴u.
equivalence, i.e. s.t. the simplification 𝑄 of 𝑃 only needs to
stay equivalent under addition of any 𝑅 over a relativized Definition 2.12 (Saribatur and Woltran (2024)).
signature 𝐵 Ď Σ.
FrSS :“ tf | ℋ𝒯 𝐴,𝐵 pfp𝑃, 𝐴, 𝐵qq “ tx𝑋, 𝑌 y |
Definition 2.5 (Woltran (2004)). A pair of interpretations č 𝑌
𝑌 Ď Σz𝑉 ^ 𝑋 P ℛx𝑃,𝐴,𝐵y u,
x𝑋, 𝑌 y is a (relativized) B-HT-interpretation iff either 𝑋 “ 𝑌
or 𝑋 Ă p𝑌 z𝐵q. The former are called total and the latter non- for all programs 𝑃 and 𝐴, 𝐵 Ď Σu
total B-HT-interpretations. Moreover, a B-HT-interpretation
x𝑋, 𝑌 y is a (relativized) B-HT-model of a program 𝑃 iff: The class FrSS satisfies prSPq whenever possible.
1. 𝑌 |ù 𝑃 ; Theorem 2.13 (Saribatur and Woltran (2024)). Every
2. for all 𝑌 1 Ă 𝑌 with p𝑌 1 z𝐵q “ p𝑌 z𝐵q : 𝑌 1 |ù 𝑃 𝑌 ; f P FrSS satisfies prSPqx𝑃,𝐴,𝐵y , 𝐵 Ď 𝐴, for every relativized
and
forgetting instance x𝑃, 𝐴, 𝐵y, where 𝑃 does not satisfy
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 pro- The following theorem confirms that forgetting can be
grams 𝑃1 and 𝑃2 are strongly equivalent relative to 𝐵 iff used as a stepping-stone to, more generally, derive 𝐵-
ℋ𝒯 𝐵 p𝑃1 q “ ℋ𝒯 𝐵 p𝑃2 q. relativized 𝐴-simplifications.
Definition 2.6 (Saribatur and Woltran (2024)). Given Theorem 2.14 (Saribatur and Woltran (2024)). Let
𝑃 over Σ, 𝐴, 𝐵 Ď Σ, and 𝑄 over Σz𝐴, 𝑄 is a (strong) 𝑃 be 𝐵-relativized 𝐴-simplifiable, and f P FrSS . Then
𝐴-simplification of 𝑃 relative to 𝐵 if for any program 𝑅 fp𝑃||𝐴X𝐵 , 𝐴z𝐵, 𝐵z𝐴q is a 𝐵-relativized 𝐴-simplification
over 𝐵 that is 𝐴-separated: of 𝑃 .
𝒜𝒮p𝑃 Y 𝑅q||𝐴 “ 𝒜𝒮p𝑄 Y 𝑅||𝐴 q
4
In order to streamline the presentation the original definition was
Program 𝑃 is 𝐵-relativized (strong) 𝐴-simplifiable if there slightly altered. In particular, ℋ𝒯 𝐴,𝐵 p𝑃 q behaves as if taking into
is such a 𝑄. account the complement 𝐴 ¯ of 𝐴.
2.1. Syntactic Tools There are some correspondences between the models of a
program and its rules that we can spot by this partitioning.
Defining a syntactic forgetting operators that obeys the
semantics of FrSP inevitably comes down to modifying the Proposition 2.20 (Berthold (2022)). Given a program 𝑃
existing operator fSP 5 , which is why we recall it and its in normal form over Σ, 𝑋 Ď 𝑌 Ď Σ, and an atom 𝑞 P
auxiliary constructions. For succinctness, for examples of Σ, with 𝑞 R 𝑌 , and occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y.
established definitions, we refer to [19]. Then the following equivalencies hold:
As usual [29, 30, 13, 31, 16, 17] the program is first brought
into a normal form, to avoid complications and unnecessary x𝑋, 𝑌 y |ù 𝑃 ô D𝑟 P 𝑅 Y 𝑅1 Y 𝑅4 : x𝑋, 𝑌 y |ù 𝑟
calculations caused by redundant (parts of) rules.
x𝑋𝑞, 𝑌 𝑞y |ù 𝑃 ô D𝑟 P 𝑅 Y 𝑅0 Y 𝑅2 : x𝑋𝑞, 𝑌 𝑞y |ù 𝑟
A rule 𝑟 is tautological iff H p𝑟q X B ` p𝑟q ‰ H, B ` p𝑟q X
B p𝑟q ‰ H, or B ´ p𝑟q X B ´´ p𝑟q ‰ H; 𝑟 is fundamen-
´ x𝑋, 𝑌 𝑞y |ù 𝑃 ô D𝑟 P 𝑅 Y 𝑅2 Y 𝑅3 Y 𝑅4 : x𝑋, 𝑌 𝑞y |ù 𝑟
tal, iff it is not tautological, and H p𝑟q X B ´ p𝑟q “ H and
B ` p𝑟q X B ´´ p𝑟q “ H. The next construction conversely identifies, which inter-
pretations are models of a program.
Definition 2.15 (Cabalar et al. (2007)). Given two rules 𝑟 The as-dual construction [17] generalizes constructions
and 𝑠, 𝑠 subsumes 𝑟, in symbols 𝑠 ď 𝑟, iff: that collect sets of conjunctions of literals aiming to replace
1. H p𝑠q Ď H p𝑟q Y B ´ p𝑟q, negated occurrences of a literal [15, 16].
2. B ` p𝑠q Ď B ` p𝑟q Y B ´´ p𝑟q,
3. B ´ p𝑠q Ď B ´ p𝑟q, Definition 2.21 (Berthold (2022)). Given a program 𝑃 “
4. B ´´ p𝑠q Ď B ´´ p𝑟q Y B ` p𝑟q, and t𝑟1 , . . . , 𝑟𝑛 u over Σ and an atom 𝑞 P Σ, then:
5. B ` p𝑠q X B ´´ p𝑟q “ H or H p𝑠q X H p𝑟q “ H. 𝑞
𝒟𝑎𝑠 p𝑃 q :“ tt𝑙1 , . . . , 𝑙𝑛 u |
Proposition 2.16 (Cabalar et al. (2007)). 𝑙𝑖 P 𝑛𝑜𝑡 B z𝑞 p𝑟𝑖 q Y 𝑛𝑜𝑡 𝑛𝑜𝑡 H z𝑞 p𝑟𝑖 q, 1 ď 𝑖 ď 𝑛u,
𝑟 ď 𝑠 ô ℋ𝒯 p𝑟q Ď ℋ𝒯 p𝑠q where, for a set 𝑆 of literals, 𝑛𝑜𝑡 𝑆 “ t𝑛𝑜𝑡 𝑠 | 𝑠 P 𝑆u
and 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑆 “ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑠 | 𝑠 P 𝑆u, where, for 𝑝 P Σ,
A rule 𝑟 is minimal in 𝑃 , iff it is not (strictly) subsumed
we assume the simplification 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑝 “ 𝑛𝑜𝑡 𝑝 and
by another rule 𝑠 in 𝑃 , i.e. iff ␣D𝑠 P 𝑃 : 𝑠 ď 𝑟 ^ 𝑟 ę 𝑠.
𝑛𝑜𝑡 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑝 “ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑝.
Definition 2.17. Let 𝑃 be a program. The normal form
𝑁 𝐹 p𝑃 q is obtained from 𝑃 by: By applying the as-dual to certain subsets of a program,
we are able to construct rules that point towards certain
1. removing all tautological rules; models of a program.
2. removing all atoms 𝑎 from B ´´ p𝑟q in the remaining
rules 𝑟, whenever 𝑎 P B ` p𝑟q; Proposition 2.22 (Berthold (2022)). Given a program 𝑃
3. removing all atoms 𝑎 from H p𝑟q in the remaining in normal form over Σ, 𝑌 Ď Σ, and an atom 𝑞 P Σ, with
rules 𝑟, whenever 𝑎 P B ´ p𝑟q; 𝑞 R 𝑌 , and occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y. Then the
4. removing from the resulting program all rules that are following implications hold:
not minimal. 𝑞
x𝑌, 𝑌 y |ù 𝑃 ñ D𝐷 P 𝒟𝑎𝑠 p𝑅1 Y 𝑅4 q : x𝑌, 𝑌 y |ù Ð 𝐷
A program 𝑃 is in normal form iff 𝑁 𝐹 p𝑃 q “ 𝑃 . 𝑞
x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃 ñ D𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 q : x𝑌 𝑞, 𝑌 𝑞y |ù Ð 𝐷
The 𝑞-exclusion notation is shorthand to remove an atom. 𝑞
x𝑌, 𝑌 𝑞y |ù 𝑃 ñ D𝐷 P 𝒟𝑎𝑠 p𝑅3 Y 𝑅4 q : x𝑌, 𝑌 𝑞y |ù Ð 𝐷
In the case that 𝑅 “ H the first and second implication hold
Definition 2.18 (𝑞-exclusion Berthold (2022)). in both directions.
Given an atom 𝑞 P Σ, and a set of literals 𝐿, a
rule 𝑟 and a program 𝑃 over Σ, the 𝑞-exclusions are The product of rules and programs are defined in order
𝐿z𝑞 :“ 𝐿zt𝑞, 𝑛𝑜𝑡 𝑞, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞u, 𝑟z𝑞 :“ H z𝑞 p𝑟q Ð B z𝑞 p𝑟q to unite their models.
and 𝑃 z𝑞 :“ t𝑟z𝑞 | 𝑟 P 𝑃 u.
Definition 2.23 (Product of Rules Berthold (2022)).
We define a partition of a program along the occurrences Let 𝑟1 and 𝑟2 be rules. Their product 𝑟1 ˆ 𝑟2 , is defined as:
of a given atom 𝑞.
H p𝑟1 q Y H p𝑟2 q Ð B p𝑟1 q Y B p𝑟2 q
Definition 2.19 (Berthold (2022)). Given a program 𝑃
in normal form over Σ and an atom 𝑞 P Σ, 𝑃 is parti- Proposition 2.24 (Berthold (2022)). Let 𝑟1 , 𝑟2 be rules
tioned according to the occurrence of 𝑞, i.e. occp𝑃, 𝑞q :“ over Σ, and 𝑋 Ď 𝑌 Ď Σ,
x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y, where:
𝑌 |ù 𝑟1 ˆ 𝑟2 ô 𝑌 |ù 𝑟1 _ 𝑌 |ù 𝑟2
𝑅 :“ t𝑟 P 𝑃 | 𝑞 R Σp𝑟qu
𝑅0 :“ t𝑟 P 𝑃 | 𝑞 P 𝐵p𝑟qu 𝑋 |ù t𝑟1 ˆ 𝑟2 u𝑌 ô 𝑋 |ù t𝑟1 u𝑌 _ 𝑋 |ù t𝑟2 u𝑌
𝑅1 :“ t𝑟 P 𝑃 | 𝑛𝑜𝑡 𝑞 P 𝐵p𝑟qu Definition 2.25 (Product of Programs Berthold (2022)).
𝑅2 :“ t𝑟 P 𝑃 | 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞 P 𝐵p𝑟q, 𝑞 R 𝐻p𝑟qu Let 𝑃1 and 𝑃2 be programs. Their product 𝑃1 ˆ 𝑃2 , is
𝑅3 :“ t𝑟 P 𝑃 | 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞 P 𝐵p𝑟q, 𝑞 P 𝐻p𝑟qu defined as:
𝑅4 :“ t𝑟 P 𝑃 | 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞 R 𝐵p𝑟q, 𝑞 P 𝐻p𝑟qu t𝑟1 ˆ 𝑟2 | 𝑟1 P 𝑃1 ^ 𝑟2 P 𝑃2 u
5
By fSP we refer to what is called fSP
˚
by Berthold (2022).
Proposition 2.26 (Berthold (2022)). Let 𝑃1 , 𝑃2 be pro- Strong subsumption is a greatest subset of regular subsump-
grams over Σ, and 𝑋 Ď 𝑌 Ď Σ, tion, to be anti-symmetric and transitive:
𝑌 |ù 𝑃1 ˆ 𝑃2 ô 𝑌 |ù 𝑃1 _ 𝑌 |ù 𝑃2 𝑠 ă 𝑟 ñ 𝑠 ă𝑠 𝑟 (3)
𝑋 |ù p𝑃1 ˆ 𝑃2 q 𝑌
ô 𝑋 |ù 𝑃1𝑌 _ 𝑋 |ù 𝑃2𝑌 𝑠 ď𝑠 𝑟 ^ 𝑟 ď𝑠 𝑡 ñ 𝑠 ď𝑠 𝑡. (4)
Strong subsumption is preserved under ˆ:
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 𝑠 ď𝑠 𝑟 ñ 𝑠 ˆ 𝑡 ď𝑠 𝑟 ˆ 𝑡 for all rules 𝑡. (5)
a classical model, and therefore whether the corresponding
As a consequence, strong subsumption is ‘modular’ in the
total model x𝑌, 𝑌 y is a potential answer set.
following sense:
Definition 2.27 (Berthold (2022)). Given a rule 𝑟, we de- 𝑠 ď𝑠 𝑟 ô @𝐴 Ď Σ : 𝑠z𝐴 ď𝑠 𝑟z𝐴 . (6)
fine the double negation of 𝑟, i.e. 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟, as:
Proof:𝑃 ‰ 𝑁 𝑃
𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 :“ Ð 𝑛𝑜𝑡 H p𝑟q Y 𝑛𝑜𝑡 𝑛𝑜𝑡 B p𝑟q
Proposition 2.28 (Berthold (2022)). Given a rule 𝑟 over p1q The requirement for ď𝑠 is stricter than that of ď.
Σ, and 𝑋 Ď 𝑌 Ď Σ, the following statement holds: p2q Follows from basic set theory and the fact that 𝑠 and
𝑟 are fundamental, and therefore H p𝑡q X B ´ p𝑡q “
𝑌 |ù 𝑟 ô x𝑋, 𝑌 y |ù 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 H “ B ` p𝑡q X B ´´ p𝑡q for 𝑡 P t𝑠, 𝑟u.
p3q The requirement for ď𝑠 is stricter than that of ď.
We would like to point out that similarly, a formula 𝜓 p4q The subset relation is transitive.
holds classically iff „„ 𝜓 holds intuitionistically. This p5q Adding literals to either part of 𝑠 and 𝑟 has no effect
connection is little surprising, given that HT-logic lies be- on the required subset-relationship.
tween classical and intuitionistic logic [27]. Further, if we p6q Is a consequence of p5q.
extend the definition of double negation over programs,
i.e. 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃 :“ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 | 𝑟 P 𝑃 u, we are able to con-
struct a program that unites the HT-models of two programs:
A rule 𝑟 is minimal in 𝑃 , iff it is not strongly subsumed
ℋ𝒯 p𝑃1 q Y ℋ𝒯 p𝑃2 q “ ℋ𝒯 pp𝑃1 Y 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃1 q ˆ p𝑃2 Y
by another rule 𝑠 in 𝑃 , i.e. iff ␣D𝑠 P 𝑃 : 𝑠 ă𝑠 𝑟.
𝑛𝑜𝑡 𝑛𝑜𝑡 𝑃2 qq.
All the aforementioned correspondences between models
Any rule 𝑟 subsumes 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟. In order not to lose dou-
and rules remain, when an atom 𝑞 is removed from a rule
ble negated rules, we therefore restrict the normal form
as well as from an interpretation.
construction 𝑁 𝐹 to its first three steps, denoted 𝑛𝑓 , when
necessary. Proposition 2.31 (Berthold 2022). Given a program 𝑃 in
We will also tweak subsumption, since as it is defined normal form over Σ, 𝑋 Ă 𝑌 Ď Σ, and an atom 𝑞 P Σ, with
above it has some properties that make it impractical to 𝑞 R 𝑌 , and occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y. Then the
use. For one, it is not anti-symmetrical, two syntactically following hold:
different rules may subsume each other, such as: 𝑟1 :“ Ð
𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎 and 𝑟2 :“ Ð 𝑎, where 𝑟1 ď 𝑟2 and 𝑟2 ď 𝑟1 . x𝑌, 𝑌 y |ù 𝑃 ô D𝑟 P 𝑅1 Y 𝑅4 : x𝑌, 𝑌 y |ù 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟z𝑞
Moreover, even though a rule may subsume another rule, _ D𝑟 P 𝑅 : x𝑌, 𝑌 y |ù 𝑟
this relation may break, when both of them are conjoined
by ˆ with the same third rule, e.g. let 𝑟3 :“ 𝑏 Ð, then x𝑋, 𝑌 y |ù 𝑃 ô D𝑟 P 𝑅 Y 𝑅1 Y 𝑅4 : x𝑋, 𝑌 y |ù 𝑟z𝑞
x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃 ô D𝑟 P 𝑅0 Y 𝑅2 : x𝑌, 𝑌 y |ù 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟z𝑞
𝑟1 ˆ 𝑟3 “ 𝑏 Ð 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎 ă 𝑏 Ð 𝑎 “ 𝑟2 ˆ 𝑟3 .
_ D𝑟 P 𝑅 : x𝑌, 𝑌 y |ù 𝑟
To avoid these issues, we define a stricter version of sub- x𝑌, 𝑌 𝑞y |ù 𝑃 ô x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃
sumption.
_ D𝑟 P 𝑅3 Y 𝑅4 : x𝑌, 𝑌 y |ù 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟z𝑞
Definition 2.29. Given two fundamental rules 𝑟 and 𝑠, 𝑠 x𝑌, 𝑌 𝑞y |ù 𝑃 ô x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃
strongly subsumes 𝑟, in symbols 𝑠 ď𝑠 𝑟, iff: 𝑞
^ D𝐷 P 𝒟𝑎𝑠 p𝑅3 Y 𝑅4 q : x𝑌, 𝑌 y |ù Ð 𝐷
1. H p𝑠q Ď H p𝑟q Y B ´ p𝑟q, x𝑋𝑞, 𝑌 𝑞y |ù 𝑃 ô D𝑟 P 𝑅 Y 𝑅0 Y 𝑅2 : x𝑋, 𝑌 y |ù 𝑟z𝑞
2. B ` p𝑠q Ď B ` p𝑟q, x𝑋, 𝑌 𝑞y |ù 𝑃 ô x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃
3. B ´ p𝑠q Ď B ´ p𝑟q, and
_ D𝑟 P 𝑅 Y 𝑅2 Y 𝑅3 Y 𝑅4 : x𝑋, 𝑌 y |ù 𝑟z𝑞
4. B ´´ p𝑠q Ď B ´´ p𝑟q Y B ` p𝑟q.
Then 𝑠 ă𝑠 𝑟, iff 𝑠 ď𝑠 𝑟 ^ 𝑠 ‰ 𝑟. If additionally 𝑅 “ H, then
𝑞
x𝑌, 𝑌 y |ù 𝑃 ô D𝐷 P 𝒟𝑎𝑠 p𝑅1 Y 𝑅4 q : x𝑌, 𝑌 y |ù Ð 𝐷
Proposition 2.30. Strong subsumption is finer than regular 𝑞
subsumption: x𝑌 𝑞, 𝑌 𝑞y |ù 𝑃 ô D𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 q : x𝑌, 𝑌 y |ù Ð 𝐷
For all 𝑟2 P 𝑅2 :
𝑠 ď𝑠 𝑟 ñ 𝑠 ď 𝑟 (1)
x𝑌 𝑞, 𝑌 𝑞y |ù 𝑟2 ô x𝑌, 𝑌 𝑞y |ù 𝑟2 , and
Strong subsumption is anti-symmetric:
x𝑋𝑞, 𝑌 𝑞y |ù 𝑟2 ô x𝑋, 𝑌 𝑞y |ù 𝑟2 .
𝑠 ď𝑠 𝑟 ^ 𝑟 ď𝑠 𝑠 ñ 𝑠 “ 𝑟. (2) The rules identified in Prop. 2.31 constitute the essential
pillars of defining forgetting operators.
2.2. Syntactic Forgetting with pSPq The operator fW , which contradicts any x𝑋, 𝑌 y for which
y ‰ H and 𝑋 R ℛx𝑃,𝑉 y , is again defined by induc-
𝑌 𝑌
𝑅𝑒𝑙x𝑃,𝑉
Given that the semantics of FrSP and FSP coincide for some
tion. By uniting fR with fW , we are then able to construct
inputs, it is not surprising that a representative of FrSP needs
fSP .
to be a modification of fSP . We, hence, recall its construc-
tion [19]. The operator fSP is defined via two auxiliary opera- Definition 2.39 (fW`
). Given a program 𝑃 in normal form
tors fR and fW , each of which is again defined using auxiliary over Σ and 𝑞 P Σ s.t. occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y,
operators fR𝐴 and fW 𝐴
, which are defined inductively. then:
`
Definition 2.32 (fR` ). Given a program 𝑃 in normal form fW p𝑃, 𝑞q :“ 𝑁 𝐹 p1 Y 2q
over Σ and 𝑞 P Σ s.t. occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y.
where:
Then:
1 :“ tp𝑟0 ˆ 𝑟1 ˆ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟qz𝑞 ˆ Ð 𝐷 |
fR` p𝑃, 𝑞q :“ 𝑛𝑓 p1 Y 2 Y 3 Y 4q
𝑞
𝑟0 P 𝑅0 , 𝑟, 𝑟1 P 𝑅3 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 qu
where: asd
𝑞 2 :“ tp𝑟 ˆ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟1 qz𝑞 ˆ Ð 𝐷 |
1 :“ tÐ 𝐷 | 𝐷 P 𝒟𝑎𝑠 p𝑅3 Y 𝑅4 qu
𝑞
𝑟 P 𝑅 Y 𝑅2 , 𝑟1 P 𝑅3 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 qu
2 :“ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟z𝑞 | 𝑟 P 𝑅0 Y 𝑅2 u
´
Definition 2.40 (fW ). Given a program 𝑃 in normal form
3 :“ t𝑟z𝑞 | 𝑟 P 𝑅 Y 𝑅2 u
over Σ and 𝑞 P Σ s.t. occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y,
4 :“ tp𝑟0 ˆ 𝑟1 qz𝑞 | 𝑟0 P 𝑅0 , 𝑟1 P 𝑅3 Y 𝑅4 u then:
´
Proposition 2.33. Given a program 𝑃 over Σ, an atom 𝑞 P fW p𝑃, 𝑞q :“ 𝑁 𝐹 p1q
Σ, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σzt𝑞u, then:
where:
𝑌
x𝑌, 𝑌 y |ù fR` p𝑃, 𝑞q ô t𝑞u P 𝑅𝑒𝑙x𝑃,t𝑞uy 𝑞
1 :“ t𝑟1z𝑞 ˆ Ð 𝐷 | 𝑟1 P 𝑅 Y 𝑅1 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅1 Y 𝑅4 qu
𝑌
If t𝑞u P 𝑅𝑒𝑙x𝑃,t𝑞uy , then: 𝐴
Definition 2.41 (fW ). Let 𝑃 be a program over Σ, and
x𝑋, 𝑌 y |ù fR` p𝑃, 𝑞q ô x𝑋𝑞, 𝑌 𝑞y |ù 𝑃 _ x𝑋, 𝑌 𝑞y |ù 𝑃 𝐴 Ď t𝑞1 , 𝑞2 , . . . , 𝑞𝑛 u “ 𝑉 Ď Σ, s.t. 0 ă 𝑛, then:
𝐴
Definition 2.34 (fR´ ). Given a program 𝑃 in normal form fW p𝑃, Hq :“ 𝑃
over Σ and 𝑞 P Σ s.t. occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y. 𝐴 b𝑛 𝐴 z𝑞𝑛
fW p𝑃, 𝑉 q :“ fW pfW p𝑃 z𝑅, 𝑉 zt𝑞𝑛 uq, 𝑞𝑛 q Y 𝑅
Then:
fR´ p𝑃, 𝑞q :“ 𝑛𝑓 p1 Y 2q where:
#
`
where: b𝑛 fW , if 𝑞𝑛 P 𝐴
fW :“ ´
fW , otherwise
1 :“ t𝑟1z𝑞 | 𝑟1 P 𝑅 Y 𝑅1 Y 𝑅4 u
𝑅 :“ t𝑟 P 𝑃 | 𝑉 X Σp𝑟q “ Hu
2 :“ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟1z𝑞 | 𝑟1 P 𝑅1 Y 𝑅4 u
Proposition 2.42. Given a program 𝑃 over Σ, and sets 𝑋,
The operators fR𝐴 is defined inductively by nested calls on 𝑌 , 𝐴 and 𝑉 , s.t. 𝐴 Ď 𝑉 Ď Σ, 𝑋 Ď 𝑌 Ď Σz𝑉 , and
fR` and fR´ . In order to fix a concrete forgetting result, we 𝑅 “ t𝑟 P 𝑃 | 𝑉 X Σp𝑟q “ Hu “ H, then:
assume an arbitrary order on 𝑉 , which has no effect on the 𝑌 2 2
following propositions. 𝐴 P 𝑅𝑒𝑙x𝑃,𝑉 y ^ @𝐴 Ď 𝐴 : x𝑋𝐴 , 𝑌 𝐴y |ù 𝑃
𝐴
Definition 2.35 (fR𝐴 ). Let 𝑃 be a program over Σ, and ô x𝑋, 𝑌 y |ù fW p𝑃, 𝑉 q
𝐴 Ď t𝑞1 , 𝑞2 , . . . , 𝑞𝑛 u “ 𝑉 Ď Σ, s.t. 0 ă 𝑛, then: Definition 2.43 (fW ). Given a program 𝑃 in normal form
fR𝐴 p𝑃, Hq :“ 𝑃 over Σ and 𝑉 Ď Σ. Then:
ď 𝐴
z𝑞𝑛
fR𝐴 p𝑃, 𝑉 q :“ fRb𝑛 pfR𝐴 p𝑃, 𝑉 zt𝑞𝑛 uq, 𝑞𝑛 q fW p𝑃, 𝑉 q :“ 𝑁 𝐹 p fW p𝑃, 𝑉 qq
𝐴Ď𝑉
where: ˚
# Definition 2.44 (fSP ). Let 𝑃 be a program over Σ in normal
fR` , if 𝑞𝑛 P 𝐴 form and 𝑉 Ď Σ.
fRb𝑛 :“
fR´ , otherwise
fSP p𝑃, 𝑉 q :“ 𝑁 𝐹 pfW p𝑃, 𝑉 q Y fR p𝑃, 𝑉 qq
Proposition 2.36. Given a program 𝑃 over Σ, and sets 𝑋, Example 2.45. Let 𝑃2.45 “ t𝑎 Ð 𝑏, 𝑞; 𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑞; 𝑞 Ð
𝑌 , 𝐴 and 𝑉 , s.t. 𝐴 Ď 𝑉 Ď Σ, and 𝑋 Ď 𝑌 Ď Σz𝑉 , then 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑞u, and 𝑉 “ t𝑝, 𝑞u. Then fSP p𝑃, 𝑉 q can be derived
x𝑌, 𝑌 y |ù fR𝐴 p𝑃, 𝑉 q ô 𝐴 P 𝑅𝑒𝑙x𝑃,𝑉
𝑌
y by:
𝑌 t𝑞u t𝑞u
If 𝐴 P 𝑅𝑒𝑙x𝑃,𝑉 y , then: fR p𝑃, 𝑉 q Ď t𝑐 Ð 𝑑u fW p𝑃, 𝑉 q “ t𝑎 Ð 𝑏, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎u
x𝑋, 𝑌 y |ù fR𝐴 p𝑃, 𝑉 q ô D𝐴2 Ď 𝐴 : x𝑋𝐴2 , 𝑌 𝐴y |ù 𝑃 fRH p𝑃, 𝑉 q Ď t𝑎 Ð 𝑏u H
fW p𝑃, 𝑉 q “ t𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑐u
Definition 2.37 (fR ). Let 𝑃 be a program over Σ in normal t𝑞u
fSP p𝑃, 𝑉 q “ 𝑁 𝐹 pfR p𝑃, 𝑉 q ˆ fRH p𝑃, 𝑉 q
form and 𝑉 Ď Σ.
t𝑞u H
ą 𝐴 Y fW p𝑃, 𝑉 q Y fW p𝑃, 𝑉 qq
fR p𝑃, 𝑉 q :“ 𝑁 𝐹 p f𝑅 p𝑃, 𝑉 qq
𝐴Ď𝑉 “ t𝑎 _ 𝑐 Ð 𝑏, 𝑑; 𝑎 Ð 𝑏, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑎; 𝑐 Ð 𝑑, 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑑u
Theorem 2.38. fR P FR Theorem 2.46. fSP P FSP
3. Towards Syntactic Forgetting Proposition 3.2. Given a program 𝑃 over Σ, an atom 𝑐 P
Σ, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σ, then:
with prSPq
𝑌 |ù gR` p𝑃, 𝑐q ô 𝑌 |ù 𝑃 ^ 𝑐 P 𝑌 ^ 𝑌 zt𝑐u |ù 𝑃 𝑌
The idea in the following constructions is to modify the
results of the previous operators, to take into account a set If 𝑌 |ù gR` p𝑃, 𝑐q, then:
𝐵 to relativize to. As witnessed in the previous section, half
x𝑋, 𝑌 y |ù fR` p𝑃, 𝑞q ô x𝑋, 𝑌 y |ù 𝑃
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. Definition 3.3 (gR´ ). Given a program 𝑃 in normal form
over Σ and 𝑐 P Σ s.t. occp𝑃, 𝑐q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y.
FrR :“ tf | ℋ𝒯 𝐴,𝐵 pfp𝑃, 𝐴, 𝐵qq “ tx𝑋, 𝑌 y |
ď 𝑌 Then:
𝑌 Ď Σz𝑉 ^ 𝑋 P ℛx𝑃,𝐴,𝐵y u,
gR´ p𝑃, 𝑐q :“ 𝑛𝑓 p1 Y 2 Y 3q
for all programs 𝑃 and 𝐴, 𝐵 Ď Σu
where:
While the ‘r’ in prSPq and the ‘R’ in FR both mean ‘rela- 1 :“ t𝑟1 | 𝑟1 P 𝑅 Y 𝑅1 Y 𝑅4 u
tivized’, it is not clear in which sense FR corresponds to the
idea of relativized equivalence. Still we use the subscript 2 :“ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟1 | 𝑟1 P 𝑅1 Y 𝑅4 u
‘rR’ for this new class in reference to its origin in FR . 3 :“ tÐ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑐u
Assume a program 𝑃 over Σ, 𝑉, 𝐵 Ď Σ, s.t. 𝑉 X 𝐵 “
H, and 𝑌 Ď 𝐵. If we take a look at the definition of the Proposition 3.4. Given a program 𝑃 over Σ, an atom 𝑐 P
class FrR , we can note that there is a similarity in how it Σ, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σ, then:
treats forgotten atoms 𝑉 and atoms that it relativizes from
Σp𝑃 qz𝐵: 𝑌 |ù gR` p𝑃, 𝑐q ô 𝑐 R 𝑌 ^ 𝑌 |ù 𝑃
• Given 𝐴 Ď 𝑉 , a total model x𝑌 𝐴, 𝑌 𝐴y of 𝑃 , s.t. If 𝑌 |ù gR` p𝑃, 𝑐q, then:
there is a 𝐴1 Ď 𝐴 with x𝑌 𝐴1 , 𝑌 𝐴y |ù 𝑃 is not
x𝑋, 𝑌 y |ù gR´ p𝑃, 𝑐q ô x𝑋, 𝑌 y |ù 𝑃
considered by ℛ𝑌x𝑃,𝑉,𝐵y ;
• Similarly, given 𝐶 Ď Σp𝑃 qzp𝐵 Y 𝑉 q, a total model As before, in order to fix a concrete forgetting result, we
x𝑌 𝐶, 𝑌 𝐶y of 𝑃 , s.t. there is a 𝐶 1 Ď 𝐶 with assume an arbitrary order on 𝐶.
x𝑌 𝐶 1 , 𝑌 𝐶y |ù 𝑃 is not considered by ℛ𝑌x𝑃,𝑉,𝐵y ,
Definition 3.5 (gR𝐶 ). Let 𝑃 be a program over Σ, 𝐵 Ď Σ
by the construction of ℋ𝒯 𝐵 p𝑃 q.
and
The operator fR includes an encoding for the first bullet- ¯ :“ Σp𝑃 qz𝐵, s.t. 0 ă 𝑛, then:
𝐶 Ď t𝑐1 , 𝑐2 , . . . , 𝑐𝑛 u “ 𝐵
point. The key-idea therefore is to manipulate the auxiliary
gR𝐶 p𝑃, Hq :“ 𝑃
constructions of fR further, to encode the second bullet-
z𝑐𝑛
point. gR𝐶 p𝑃, 𝐵q :“ gRb𝑛 pgR𝐶 p𝑃, 𝐶zt𝑐𝑛 uq, 𝑐𝑛 q
For each 𝐴 Ď 𝑉 and 𝐶 Ď Σp𝑃 qzp𝐵 Y 𝑉 q, we de-
fine an auxiliary operator gR𝐴,𝐶 that determines for any where:
𝑌 Ď pΣp𝑃 q X 𝐵qz𝑉 whether (i) 𝑌 Y 𝐴 Y 𝐶 |ù 𝑃 ,
#
gR` , if 𝑐𝑛 P 𝐶
and whether (ii) there are no 𝐴1 Ď 𝐴 and 𝐶 1 Ď 𝐶, s.t. gRb𝑛 :“
gR´ , otherwise
𝐴1 Y 𝐵 1 Ă 𝐴 Y 𝐵, and x𝑌 𝐴1 𝐶 1 , 𝑌 𝐴𝐶y |ù 𝑃 . Then
gR𝐴,𝐶 p𝑃, 𝑉 q, satisfies x𝑌 𝐶, 𝑌 𝐶y, iff (i) and (ii). Further, we
let gR𝐴,𝐶 p𝑃, 𝑉 q contradict each x𝑋𝐶 2 , 𝑌 𝐶y with 𝑋 Ă 𝑌 , Proposition 3.6. Given a program 𝑃 over Σ, sets of atoms
𝐵 Ď Σ, 𝐶 Ď 𝐵 ¯ :“ Σp𝑃 qz𝐵, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă
𝐶 2 Ď 𝐶, iff 𝑃 |ù x𝑌 𝐴1 𝐶 1 , 𝑌 𝐴𝐶y for all 𝐴1 Ă 𝐴 and
𝐶 1 Ă 𝐶. 𝑌 Ď Σ and 𝑋 Ď 𝐵, then:
The operators gR𝐴,𝐶 are defined taking into account fR𝐴 as 𝑌 |ù gR𝐶 p𝑃, 𝐵q
a baseline, i.e. gR𝐴,𝐶 p𝑃, 𝑉, 𝐵q :“ gR𝐶 pfR𝐴 p𝑃, 𝑉 q, 𝐵q. These
ô 𝑌 |ù 𝑃 ^ 𝑌 z𝐵 “ 𝐶
gR𝐶 we define inductively, starting at |𝐶| “ 1.
^ E𝑌 1 Ă 𝑌, s.t. 𝑌 1 |ù 𝑃 𝑌 and 𝑌 1 X 𝐵 “ 𝑌 X 𝐵
Definition 3.1 (gR` ). Given a program 𝑃 in normal form If 𝑌 |ù gR𝐶 p𝑃, 𝐵q, then for each 𝐶 1 Ď 𝐶:
over Σ and 𝑐 P Σ s.t. occp𝑃, 𝑐q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y.
Then: x𝑋𝐶 1 , 𝑌 y |ù gR𝐶 p𝑃, 𝐵q ô x𝑋𝐶 1 , 𝑌 y |ù 𝑃
Definition 3.7 (gR ). Let 𝑃 be a program over Σ in normal
gR` p𝑃, 𝑐q :“ 𝑛𝑓 p1 Y 2 Y 3 Y 4 Y 5q ¯ :“ Σp𝑃 qz𝐵.
form and 𝑉, 𝐵 Ď Σ. s.t. 𝑉 X 𝐵 “ H. 𝐵
where: ą 𝐴,𝐶
gR p𝑃, 𝑉, 𝐵q :“ 𝑁 𝐹 p gR p𝑃, 𝑉, 𝐵qq
𝑐 𝐴Ď𝑉
1 :“ tÐ 𝐷 | 𝐷 P 𝒟𝑎𝑠 p𝑅3 Y 𝑅4 qu ¯
𝐶Ď𝐵
2 :“ t𝑟 | 𝑟 P 𝑅 Y 𝑅2 u where
3 :“ t𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 | 𝑟 P 𝑅0 Y 𝑅2 u
gR𝐴,𝐶 p𝑃, 𝑉, 𝐵q :“ gR𝐶 pfR𝐴 p𝑃, 𝑉 q, 𝐵q
1 1
4 :“ t𝑟 | 𝑟 P 𝑅3 Y 𝑅4 u
For an illustration of how gR functions we refer to Figure 1
5 :“ tÐ 𝑛𝑜𝑡 𝑐u
on the last page.
Theorem 3.8. gR P FrR
4. Syntactic Forgetting with prSPq To define gW 𝐶
for arbitrary 𝐶 Ď Σp𝑃 qz𝐵, we assume
an arbitrary ordering on Σ, e.g. the lexicographic order,
Again we define gW s.t. it modifies an auxiliary result of and apply repeatedly the operators gW`
or gW
´
, depending
fW to take into account whether a 𝐶 Ď 𝐵 ¯ :“ Σp𝑃 qz𝐵 is on whether an atom 𝑐 is in 𝐶. For example, let 𝑃 be over
relevant. t𝑎, 𝑏, 𝑐, 𝑑u, 𝐵 “ t𝑎, 𝑏u and 𝐶 “ t𝑑u, then gW 𝐶
p𝑃, 𝐵q “
Remember, that the auxiliary operators fW 𝐴
implement a ` ´
gW pgW p𝑃, 𝑐q, 𝑑q.
check for whether 𝐴 is relevant for 𝑌 (𝐴 P 𝑅𝑒𝑙x𝑃,𝑉 𝑌
y ), i.e.
𝐶
that x𝑌 𝐴, 𝑌 𝐴y is a model of 𝑃 , but x𝑌 𝐴 , 𝑌 𝐴y is not a
1
Definition 4.5 (gW ). Let 𝑃 be a program over Σ, 𝐵 Ď Σ
model of 𝑃 for all 𝐴1 Ă 𝐴. As we have seen in the last and
section this requirement extends to relativized forgetting, in ¯ :“ Σp𝑃 qz𝐵, s.t. 0 ă 𝑛, then:
𝐶 Ď t𝑐1 , 𝑐2 , . . . , 𝑐𝑛 u “ 𝐵
the sense that we additionally need to check whether 𝑌 Y 𝐶 𝐶
can be a stable model of 𝑃 under addition of rules over 𝐵 – gW p𝑃, Hq :“ 𝑃
𝐶
gW checks, whether x𝑌 𝐶, 𝑌 𝐶y |ù 𝑃 and x𝑌 𝐶 1 , 𝑌 𝐶y |ù 𝑃 𝐶
gW b𝑛
p𝑃, 𝐵q :“ gW 𝐶
pgW
z𝑐𝑛
¯ zt𝑐𝑛 uq, 𝑐𝑛 q Y 𝑅
p𝑃 z𝑅, 𝐵
for all 𝐶 1 Ă 𝐶.
By compounding the constructions fW 𝐴
with gW𝐶
, i.e. where:
gW p𝑃, 𝑉, 𝐵q :“ gW pfW p𝑃, 𝑉 q, 𝐵q, we get operators with
𝐴,𝐶 𝐶 𝐴 #
`
the following properties. b𝑛 gW , if 𝑐𝑛 P 𝐶
gW :“
Given a program 𝑃 over Σ, 𝑉, 𝐵 Ď Σ with 𝑉 X 𝐵 “ H,
´
gW , otherwise
𝑋 Ď 𝑌 Ď Σ X 𝐵, 𝐴 Ď 𝑉 , and 𝐶 1 Ď 𝐶 Ď Σp𝑃 qz𝐵, then, 𝑅 :“ t𝑟 P 𝑃 | Σp𝑟q Ď 𝐵u
𝐴,𝐶
gW p𝑃, 𝑉, 𝐵q contradicts x𝑋𝐶 1 , 𝑌 𝐶y i.e. x𝑋𝐶 1 , 𝑌 𝐶y |ù
gW p𝑃, 𝑉, 𝐵q, iff x𝑌 𝐶𝐴, 𝑌 𝐶𝐴y |ù 𝑃 , for all 𝐴1 Ď 𝐴 and
𝐴,𝐶
The fact that the properties of gW
`
and gW
´
extend to gW
𝐶
𝐶 2 Ď 𝐶 with 𝐴1 Y 𝐶 2 Ă 𝐴 Y 𝐶: x𝑌 𝐴1 𝐶 2 , 𝑌 𝐴𝐶y |ù 𝑃 , can be checked rather straight-forwardly by induction.
and for all 𝐴1 Ď 𝐴: x𝑋𝐶 1 𝐴1 , 𝑌 𝐴𝐶y |ù 𝑃 .
The auxiliary operators gW𝐴
are again inductively defined Proposition 4.6. Given a program 𝑃 over Σ, sets of atoms
via gW and gW .
` ´
𝐵 Ď Σ, 𝐶 Ď Σp𝑃 qz𝐵, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σ,
then:
`
Definition 4.1 (gW ). Given a program 𝑃 in normal form
𝐶
over Σ and 𝑐 P Σ s.t. occp𝑃, 𝑐q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y, x𝑋, 𝑌 y |ù gW p𝑃, 𝐵q
then: ô 𝑌 |ù 𝑃 ^ 𝑌 z𝐵 “ 𝐶
`
gW p𝑃, 𝑐q :“ 𝑁 𝐹 p1 Y 2q ^ E𝑌 1 Ă 𝑌, s.t. 𝑌 1 |ù 𝑃 𝑌 and 𝑌 1 X 𝐵 “ 𝑌 X 𝐵
^ x𝑋, 𝑌 y |ù 𝑃
where:
To construct gW , fW𝐴
and gW𝐶
are compounded for each
1 :“ t𝑟1 ˆ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟 ˆ Ð 𝐷 |
𝐴 Ď 𝑉 and 𝐶 Ď Σp𝑃 qz𝐵, i.e. gW 𝐴,𝐶
p𝑃, 𝑉, 𝐵q :“
𝑐
𝑟, 𝑟1 P 𝑅3 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 qu pfW p𝑃, 𝑉 q, 𝐵q. The resulting rules of each of these com-
𝐶 𝐴
gW
2 :“ tp𝑟 ˆ 𝑛𝑜𝑡 𝑛𝑜𝑡 𝑟1 q ˆ Ð 𝐷 | pounds are then united.
𝑐
𝑟 P 𝑅 Y 𝑅2 , 𝑟1 P 𝑅3 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅0 Y 𝑅2 qu Definition 4.7 (gW ). Given a program 𝑃 in normal form
over Σ and 𝑉 Ď Σ. Then:
The building-blocks gW `
and gW
´
of our inductive definition ď 𝐴,𝐶
take into account one atom that is relativized away. We can gW p𝑃, 𝑉, 𝐵q :“ 𝑁 𝐹 p gW p𝑃, 𝑉, 𝐵qq
therefore again use the observations of Prop. 2.31 to see that 𝐴Ď𝑉
¯
𝐶Ď𝐵
for the case |𝐶| “ 1 they have the desired properties.
where:
Proposition 4.2. Given a program 𝑃 over Σ, an atom 𝑐 P
𝐴,𝐶 𝐶 𝐴
Σ, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σ, then: gW p𝑃, 𝑉, 𝐵q :“ gW pfW p𝑃, 𝑉 q, 𝐵q
x𝑋, 𝑌 y |ù gR` p𝑃, 𝑐q We would like to remark here that, while this construction
𝑌 may appear rather costly computationally, some factors that
ô 𝑌 |ù 𝑃 ^ 𝑐 P 𝑌 ^ 𝑌 zt𝑐u |ù 𝑃 ^ x𝑋, 𝑌 y |ù 𝑃 may dampen the blow-up that have been discussed in non-
´ relativized forgetting [19], also apply here.
Definition 4.3 (gW ). Given a program 𝑃 in normal form
Most importantly, the operator gW 𝐴,𝐶
is such that its re-
over Σ and 𝑞 P Σ s.t. occp𝑃, 𝑞q “ x𝑅, 𝑅0 , 𝑅1 , 𝑅2 , 𝑅3 , 𝑅4 y,
sult is the empty program, if the combination 𝐴, 𝐶 is ‘non-
then:
relevant’. If this ‘non-relevancy’ is detected within a recur-
´
gW p𝑃, 𝑐q :“ 𝑁 𝐹 p1q sive step of gW 𝐴,𝐶
possibly exponentially many calculations
can be disregarded.
where: More concretely, assume for example a program 𝑃 over
t𝑎, . . . , 𝑧u, 𝑉 “ t𝑝, . . . , 𝑧u and 𝐵 “ t𝑎, . . . , ℎu. If
𝑞
1 :“ t𝑟1 ˆ Ð 𝐷 | 𝑟1 P 𝑅 Y 𝑅1 Y 𝑅4 , 𝐷 P 𝒟𝑎𝑠 p𝑅1 Y 𝑅4 qu `
fW p𝑃, 𝑝q “ H, then gW 𝐴,𝐶
p𝑃, 𝑉, 𝐵q will be the empty pro-
gram for any 𝐴 Ě t𝑝u and any 𝐶, which lets us disregard a
large part of the recursive calculation-tree.
Proposition 4.4. Given a program 𝑃 over Σ, an atom 𝑐 P
Σ, and sets 𝑋 and 𝑌 , s.t. 𝑋 Ă 𝑌 Ď Σ, then: Definition 4.8 (frSP ). Let 𝑃 be a program over Σ in normal
form and 𝑉 Ď Σ.
x𝑋, 𝑌 y |ù gR´ p𝑃, 𝑐q
ô 𝑐 R 𝑌 ^ 𝑌 |ù 𝑃 ^ x𝑋, 𝑌 y |ù 𝑃 frSP p𝑃, 𝑉 q :“ 𝑁 𝐹 pgW p𝑃, 𝑉 q Y gR p𝑃, 𝑉 qq
Theorem 4.9. frSP P FrSS
Corollary 4.10. Let 𝑃 be 𝐵-relativized 𝐴-simplifiable, then
frSP p𝑃||𝐴X𝐵 , 𝐴z𝐵, 𝐵q is a 𝐵-relativized 𝐴-simplification of
𝑃.
5. Let’s not Forget about Predicates
It remains an open question, as to how forgetting proposi-
tional 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 for- x𝑎𝑏𝑐ℎ𝑞, 𝑎𝑏𝑐ℎ𝑞y x𝑎𝑏𝑐𝑞, 𝑎𝑏𝑐𝑞y
getting about terms, ground atoms, or predicate symbols, x𝑎𝑏ℎ, 𝑎𝑏𝑐ℎ𝑞y x𝑎𝑏𝑐, 𝑎𝑏𝑐𝑞y
where the latter probably comes closest to the propositional x𝑎, 𝑎𝑏𝑐𝑞y
case. When forgetting about predicate symbols, two obsta-
cles come to mind. (i) A predicate may be recursive, making
it impossible to find a (finite) forgetting result. E.g.: consider x𝑎𝑏𝑐ℎ, 𝑎𝑏𝑐ℎy x𝑎𝑏𝑐, 𝑎𝑏𝑐y
forgetting 𝑡 from the following program: x𝑎𝑏𝑐, 𝑎𝑏𝑐ℎy x𝑎, 𝑎𝑏𝑐y
𝑡p𝑋, 𝑌 q Ð 𝑒p𝑋, 𝑌 q. 𝑎p𝑋, 𝑌 q Ð 𝑡p𝑋, 𝑌 q, 𝑏p𝑋, 𝑌 q. x𝑎ℎ, 𝑎𝑏𝑐ℎy
𝑡p𝑋, 𝑍q Ð 𝑡p𝑋, 𝑌 q, 𝑒p𝑌, 𝑍q.
One may consider finite forgetting results that have desir-
able properties up to some bound, as has been similarly done t𝑞u
fR p𝑃, 𝑉 q
for classical logic [32]. (ii) Even if a non-recursive predicate
symbol is forgotten we may have to leave the class of logic x𝑎𝑏𝑐ℎ, 𝑎𝑏𝑐ℎy
programs to represent a result of forgetting. E.g. consider x𝑎𝑏ℎ, 𝑎𝑏𝑐ℎy
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. x𝑎𝑏𝑐ℎ, 𝑎𝑏𝑐ℎy x𝑎𝑏𝑐, 𝑎𝑏𝑐y
𝑎p𝑋, 𝑌 q Ð 𝑛𝑜𝑡 𝑏p𝑋, 𝑌 q, 𝑛p𝑋q, 𝑛p𝑌 q. 𝑛p𝑌 q Ð 𝑒p𝑋, 𝑌 q. x𝑎𝑏𝑐, 𝑎𝑏𝑐ℎy x𝑎, 𝑎𝑏𝑐y
x𝑎ℎ, 𝑎𝑏𝑐ℎy
A possible forgetting result in full first order syntax is 𝜓:
@𝑋, 𝑍 : p␣D𝑌 : p𝑒p𝑋, 𝑌 q ^ 𝑒p𝑌, 𝑍qq ^ 𝑛p𝑋q ^ 𝑛p𝑌 q fRH p𝑃, 𝑉 q
Ñ 𝑎p𝑋, 𝑍q
tℎu t𝑞u H t𝑞u
gR pfR p𝑃, 𝑉 q, 𝐵q gR pfR p𝑃, 𝑉 q, 𝐵q
^ 𝑒p𝑋, 𝑍q Ñ p𝑛p𝑋q ^ 𝑛p𝑍qqq
x𝑎𝑏𝑐ℎ, 𝑎𝑏𝑐ℎy
where the impossiblility of 𝜓 to be put into a prenex-
normalform, is inherited from intuitionism. It may be worth- x𝑎𝑏ℎ, 𝑎𝑏𝑐ℎy H
while to consider subclasses of the full first-order syntax x𝑎𝑏, 𝑎𝑏𝑐ℎy
that are well behaved w.r.t. forgetting. Related to this ques-
tion there are two extensions of logic programs that are able
to capture the full polynomial hierarchy, stable-unstable x𝑎𝑏𝑐, 𝑎𝑏𝑐y
programs [33] and logic programs with quantifiers [34]. A H x𝑎, 𝑎𝑏𝑐y
relaxed version of forgetting from logic programs, so-called
interpolation has recently been successfully reduced to the
classical case [35]. tℎu
gR pfRH p𝑃, 𝑉 q, 𝐵q
H H
gR pfR p𝑃, 𝑉 q, 𝐵q
6. Conclusion gR p𝑃, 𝑉, 𝐵q
The question on how a logic program may be simplified, has x𝑎𝑏𝑐ℎ, 𝑎𝑏𝑐ℎy x𝑎𝑏𝑐, 𝑎𝑏𝑐y
become a rather large one, sparking several subtopics that x𝑎𝑏ℎ, 𝑎𝑏𝑐ℎy x𝑎, 𝑎𝑏𝑐y
cover different particular aims: forgetting, abstraction, sim- x𝑎𝑏, 𝑎𝑏𝑐ℎy
plification. These ideas have recently been captured under
an umbrella-term of (strong) 𝐴-simplifications of 𝑃 rela-
tivized to 𝐵 [25]. The existence of this more abstract version Figure 1: This figure illustrates how gR takes a divide and con-
of forgetting tore open a hole between the semantics and quer approach to be able to encode the semantics of FrR . Here
syntax that that was just recently closed [19]. In this paper we abstract away from the specific syntax of each auxiliary pro-
we were able to close it again by intricately modifying fSP , gram and only look at their models. For each set of models in
to be able to take into account a relativization set. Given that a box such a representative exists [13]. The models of an initial
most of the recent results are limited to the propositional program 𝑃 are on the top most box, the models of the auxiliary
case, we believe that it would be interesting to explore how results of forgetting 𝑉 “ t𝑞u relativized to 𝐵 “ t𝑎, 𝑏, 𝑐u are
they translate to forgetting about predicate-symbols next. listed from there on downward. The workings of frSP follow a
similar pattern, but are hard to put into an illustration, since the
𝑉,𝐵
auxiliary operators gW satisfy a lot more models.
Acknowledgements sistence, Theory and Practice of Logic Programming
(2019). doi:10.1017/S1471068419000346.
This work was supported by the German Federal Ministry [18] R. Gonçalves, T. Janhunen, M. Knorr, J. Leite,
of Education and Research (BMBF, 01IS18026B-F) by fund- On syntactic forgetting under uniform equivalence,
ing the competence center for Big Data and AI “ScaDS.AI” in: Proceedings of (JELIA-21), 2021. doi:10.1007/
Dresden/Leipzig. 978-3-030-75775-5\_20.
[19] M. Berthold, On syntactic forgetting with strong per-
sistence, in: Proceedings of (KR-22), 2022.
References [20] F. Aguado, P. Cabalar, J. Fandinno, D. Pearce, G. Pérez,
[1] A. Heyting, Die formalen regeln der intuitionis- C. Vidal, Syntactic ASP forgetting with forks, Ar-
tischen logik, in: Sitzungsberichte der Preussis- tificial Intelligence (2024). doi:10.1016/J.ARTINT.
chen Akademie der Wissenschaften. Physikalisch- 2023.104033.
mathematische Klasse, 1930. [21] Z. G. Saribatur, T. Eiter, Omission-based abstraction
[2] V. Lifschitz, D. Pearce, A. Valverde, A characterization for answer set programs, in: Proceedings of (KR-18),
of strong equivalence for logic programs with vari- 2018.
ables, in: Proceedings of (LPNMR-07), 2007. doi:10. [22] T. Eiter, Z. G. Saribatur, P. Schüller, Abstraction for
1007/978-3-540-72200-7\_17. zooming-in to unsolvability reasons of grid-cell prob-
[3] Y. Chen, Y. Zhang, Y. Zhou, First-order indefinabil- lems, CoRR (2019). arXiv:1909.04998.
ity of answer set programs on finite structures, in: [23] Z. G. Saribatur, T. Eiter, A semantic perspective on
Proceedings of (AAAI-10), 2010. omission abstraction in ASP, in: Proceedings of (KR-
[4] F. Lin, R. Reiter, Forget it, in: Working Notes of AAAI 20), 2020. doi:10.24963/KR.2020/75.
Fall Symposium on Relevance, 1994. [24] Z. G. Saribatur, S. Woltran, Foundations for projecting
[5] J. P. Delgrande, A knowledge level account of forget- away the irrelevant in ASP programs, in: Proceedings
ting, Journal of Artificial Intelligence Research (2017). of (KR-23), 2023. doi:10.24963/KR.2023/60.
doi:10.1613/jair.5530. [25] Z. G. Saribatur, S. Woltran, A unified view on for-
[6] T. Eiter, G. Kern-Isberner, A brief survey on forget- getting and strong equivalence notions in answer set
ting from a knowledge representation and reason- programming, in: Proceedings of (AAAI-24), 2024.
ing perspective, KI - Künstliche Intelligenz (2018). doi:10.1609/AAAI.V38I9.28940.
doi:10.1007/s13218-018-0564-6. [26] V. Lifschitz, L. R. Tang, H. Turner, Nested expres-
[7] R. Gonçalves, M. Knorr, J. Leite, The ultimate guide to sions in logic programs, Annals of Mathematics
forgetting in answer set programming, in: Proceedings and Artificial Intelligence (1999). doi:10.1023/A:
of (KR-16), 2016. 1018978005636.
[8] R. Gonçalves, M. Knorr, J. Leite, You can’t always [27] V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent
forget what you want: On the limits of forgetting in logic programs, ACM Transactions on Computational
answer set programming, in: Proceedings of (ECAI-16), Logic (2001).
2016. doi:10.3233/978-1-61499-672-9-957. [28] S. Woltran, Characterizations for relativized no-
[9] R. Gonçalves, M. Knorr, J. Leite, S. Woltran, When you tions of equivalence in answer set programming,
must forget: Beyond strong persistence when forget- in: Proceedings of (JELIA-04), 2004. doi:10.1007/
ting in answer set programming, Theory and Practice 978-3-540-30227-8\_16.
of Logic Programming (2017). [29] K. Inoue, C. Sakama, Negation as failure in the head,
[10] R. Gonçalves, T. Janhunen, M. Knorr, J. Leite, Journal of Logic Programming (1998).
S. Woltran, Forgetting in modular answer set pro- [30] K. Inoue, C. Sakama, Equivalence of logic programs
gramming, in: Proceedings of (AAAI-19), 2019. doi:10. under updates, in: Proceedings of (JELIA-04), 2004.
1609/aaai.v33i01.33012843. [31] M. Slota, J. Leite, Back and forth between rules and
[11] R. Gonçalves, T. Janhunen, M. Knorr, J. Leite, On syn- SE-models, in: Proceedings of (LPNMR-11), 2011.
tactic forgetting under uniform equivalence, in: Pro- [32] Y. Zhou, Y. Zhang, Bounded forgetting, in: Proceed-
ceedings of (JELIA-21), volume 12678, 2021, pp. 297– ings of (AAAI-11), 2011. doi:10.1609/AAAI.V25I1.
312. doi:10.1007/978-3-030-75775-5\_20. 7842.
[12] P. Cabalar, P. Ferraris, Propositional theories are [33] B. Bogaerts, T. Janhunen, S. Tasharrofi, Stable-unstable
strongly equivalent to logic programs, Theory and semantics: Beyond NP with normal logic programs,
Practice of Logic Programming (2007). Theory and Practice of Logic Programming (2016).
[13] P. Cabalar, D. Pearce, A. Valverde, Minimal logic pro- doi:10.1017/S1471068416000387.
grams, in: Proceedings of (ICLP-07), 2007. [34] G. Amendola, F. Ricca, M. Truszczynski, Beyond
[14] Y. Zhang, N. Y. Foo, Solving logic program conflict NP: quantifying over answer sets, Theory and
through strong and weak forgettings, Artificial Intel- Practice of Logic Programming (2019). doi:10.1017/
ligence 170 (2006) 739–778. doi:10.1016/j.artint. S1471068419000140.
2006.02.002. [35] J. Heuer, C. Wernhard, Synthesizing strongly equiv-
[15] T. Eiter, K. Wang, Semantic forgetting in answer set alent logic programs: Beth definability for answer
programming, Artificial Intelligence (2008). set programs via craig interpolation in first-order
[16] M. Knorr, J. J. Alferes, Preserving strong equivalence logic, CoRR (2024). doi:10.48550/ARXIV.2402.
while forgetting, in: Proceedings of (JELIA-14), 2014. 07696. arXiv:2402.07696.
doi:10.1007/978-3-319-11558-0_29.
[17] M. Berthold, R. Gonçalves, M. Knorr, J. Leite, A syn-
tactic operator for forgetting that satisfies strong per-