key: cord-0047141-42tdrqe7
authors: Doherty, Patrick; Szałas, Andrzej
title: Rough Forgetting
date: 2020-06-10
journal: Rough Sets
DOI: 10.1007/978-3-030-52705-1_1
sha: c9e0a7e70329075dfce2373aad7319daabe3d620
doc_id: 47141
cord_uid: 42tdrqe7

Recent work in the area of Knowledge Representation and Reasoning has focused on modification and optimization of knowledge bases (KB) through the use of forgetting operators of the form [Formula: see text], where [Formula: see text] is a set of relations in the language signature used to specify the KB. The result of this operation is a new KB where the relations in [Formula: see text] are removed from the KB in a principled manner resulting in a more efficient representation of the KB for different purposes. The forgetting operator is also reflected semantically in terms of the relation between the original models of the KB and the models for the revised KB after forgetting. In this paper, we first develop a rough reasoning framework where our KB’s consist of rough formulas with a semantics based on a generalization of Kleene algebras. Using intuitions from the classical case, we then define a forgetting operator that can be applied to rough KBs removing rough relations. A constructive basis for generating a new KB as the result of applying the forgetting operator to a rough KB is specified using second-order quantifier elimination techniques. We show the application of this technique with some practical examples.

In Artificial Intelligence, the field of Knowledge Representation and Reasoning (KRR) deals with the use of logical languages to represent knowledge or beliefs and the use of inference in some logic to derive additional knowledge or belief implicit in a base theory represented as a set of logical formulas. The explicit base theory is often called a Knowledge Base (KB). Consequences A of the KB are derived through a consequence relation, KB |= A. A signature Σ (vocabulary) is associated with the logical language and is used for specifying the legal relations, functions, constants, etc., used in the syntax of formulas.

In recent years, there has been much interest in the topic of forgetting operations in KRR [12] . Intuitions for such operators are based loosely on the fact that humans often forget what they know or believe for reasons of efficiency in reasoning. Mapping this loose intuition over to KRR results in some very powerful and useful techniques for dealing with redundant information in KB's, optimizing query retrieval in relation to KB's [10, 17] , progressing databases [18] , forgetting with description logics [6, 31] and rule based languages [26, 27] , dealing with missing information and dataset reduction [14] , forgetting sets of literals in first-order logic [28] , in addition to other techniques. In general, one major type of forgetting aims at removing information from a KB in a controlled manner where the syntactic elimination has a principled semantic correlation characterized in model theory.

Given a KB and a signature Σ, a common type of forgetting, forget(KB , Σ ), can be formulated where Σ Σ and KB is the result of forgetting the components in Σ in KB . One interesting question is the relation between the models and consequences of KB and the consequences of KB after the forgetting operation is applied to KB . Initial intuitions for this type of forgetting can be traced all the way back to Boole [2] and his use of variable elimination. Assume a propositional language with signature Σ = {p, q, r}. Given a propositional formula A and a signature Σ = {p}, the result of forgetting p in A, forget(A, Σ ),

where A + p is the result of replacing all occurrences of p in A with 'true' and A − p is the result of replacing all occurrences of p in A with 'false' and simplifying the result.

In KRR application areas such as robotics, the knowledge or beliefs robots have about different aspects of the world, is often incomplete and/or uncertain. Consequently, one wants to find a concise way to model this. Rough set theory [7, 8, 22, 23] has been used to model different types of incompleteness using indiscernibility and approximations. The general idea is to begin with a universe of individuals and define an indiscernibility relation over these individuals. In the classical case, this generates an equivalence relation over individuals. A rough set is defined by specifying a lower and upper approximation, each consisting of a number of equivalence classes generated by the indiscernibility relation. All individuals in equivalence classes included in the lower approximation are in the rough set, all equivalence classes in the upper approximation intersect with the rough set, and the individuals in the remaining equivalence classes lie outside the set. This brings to mind a division of individuals into a tripartite division reminiscent of three-valued logics. Later in the paper, this intuition will be formalized more precisely. In the context of KRR, there has been interest in generalizations of logical languages and inference to include rough logical languages and inference using rough theories [8] . This generalization will be used as a vehicle for specifying rough forgetting operators applied to rough relations in such logics.

Another application area for rough sets and logics is with big data applications. According to [14] , "most of the attribute values relating to the timing of big data [. . . ] are missing due to noise and incompleteness. Furthermore, the number of missing links between data points in social networks is approximately 80% to 90% and the number of missing attribute values within patient reports transcribed from doctor diagnoses are more than 90%."

Rough sets are discussed in [14] as one of remedies to deal with missing data. In this context, the combination of rough sets with the use of forgetting operations might prove to be very useful. In cases where important information is missing, it might be useful to forget the relation or find a relation's explicit definition andusing the definition -complete parts of the missing content. In fact, the secondorder quantifier elimination techniques which we describe in this paper and use as a tool for forgetting, provide us with definitions of eliminated (forgotten) relations as a side effect.

This paper is primarily about developing a first-order logical framework for rough theories that can be used to construct rough KB's, with a formal semantics based on rough relational structures. Given such a logic, we then define a forgetting operator that can be applied to rough theories and we provide the semantics for such an operator. The forgetting operator is based on second-order quantifier elimination techniques developed for rough theories. In previous work, we have shown how second-order quantifier elimination techniques can be automated for well-behaved fragments of second-order logic. We expand on these results in the context of rough theories.

The paper is structured as follows. In Sect. 2 we discuss the rough reasoning framework used throughout the paper. In Sect. 3, we recall definitions for forgetting used with classical logic and then generalize these and introduce rough forgetting. Next, in Sect. 4, we provide second-order quantifier elimination theorems with proofs which can serve as foundations for algorithmic techniques for rough forgetting. Section 5 provides a number of examples showing how the proposed techniques work in practice. Finally, Sect. 6 concludes the paper.

Rough sets [21, 22] have been defined in many ways (see, e.g., [4, 5, 7, 8, 16, 23, 25, 29, 30] and numerous references there). Three-and many-valued approaches have been intensively studied in the context of rough sets [3, 4, 15, 16 ]. In the current paper we will follow the presentation of [16] .

Let U be a set of objects and E be an equivalence relation on U, Then A = U, E is called an approximation space. By the lower approximation (s + ) and upper approximation (s ⊕ ) of a set s ⊆ U we mean:

In rough sets, E represents an indiscernibility relation. Approximations are interpreted as follows, where s ⊆ U is a set:

-the lower approximation s + represents objects certainly belonging to s; -the upper approximation s ⊕ represents objects possibly belonging to s.

For an approximation space A, the ordered pair s l , s u , where s l ⊆ s u and s l , s u are definable sets, is called a rough set (wrt A). 1 Remark 1. In the literature, the equivalence relation used to define rough approximations has been argued to be too strong for many application areas [8, 24, 25] . In fact, seriality of E (i.e., the property that ∀x∃y(E(x, y)) has been proposed as the weakest well-behaved requirement on E. This ensures that the lower approximation is included in the upper approximation of a rough set [11, 29] .

Note also that, according to [19, Section 19.3] , every reflexive similarity relation can be refined to an equivalence relation in a natural way. So reflexivity can be used as a basic requirement on indiscernibility relations. 2 As shown in [16] , there is a close correspondence between rough sets and Kleene algebras defined below.

is called a Kleene algebra if the following hold.

is a distributive lattice with the greatest element and the least element ⊥, and for all s, t ∈ K,

Note that in Definition 3 we refer to "greatest" and "least" elements. As usual in lattice theory, we mean the ordering:

For rough sets, a subclass of Kleene algebras, rough Kleene algebras, will have the role of Boolean algebras for classical sets.

is called a rough Kleene algebra over U iff:

By a generalized rough set we mean any element of K.

As the logical counterpart of rough Kleene algebras we will use the three valued logic of Kleene, K 3 , with truth values T (true), F (false) and U (unknown), ordered by:

with connectives ∨, ∧, ¬. The semantics of connectives is defined by:

where τ 1 , τ 2 ∈ {F, U, T} and max, min are the maximum and minimum wrt (3).

Let us now define the syntax of rough formulas used in this paper. In addition to connectives ¬, ∧, ∨ and quantifiers ∀, ∃ of Kleene logic K 3 , we add two connectives: ∈ and ⊆. Their intended meaning is rough set membership and rough set inclusion, respectively.

-Kleene formulas, KF , are defined by the grammar:

-rough formulas, RF , are defined by the grammar, where C ∪ V denotes tuples consisting of constants and/or variables:

Rough theories (rough knowledge bases) are defined below.

Definition 6 (Rough theories, rough knowledge bases). Finite sets of rough formulas are called rough theories (or rough knowledge bases). A finite set of formulas T is understood as a single formula being the conjunction of formulas in T :

Remark 2. In the rest of the paper we will often use the traditional syntax for relations. For example, rather than writing ∀x∃y (x, y) ∈ r , we will write ∀x∃y r(x, y) .

By a rough literal we mean an expression of the form ±r(ē), where ± is the empty symbol or ¬, r is a relation symbol andē is a tuple of constants and/or variables. By a rough fact we mean a rough literal not containing variables.

The following important property, justifying the use of K 3 in the context of rough forgetting, is an immediate consequence of Theorems 8, 11, 15, proved in [16] . Below:

where |= AK and A |= RS are semantic consequence relations for A K and RS, respectively.

To define the semantics of rough formulas, we first need a generalization of relational structures to their rough version.

Let U be a set of objects, K be a rough Kleene algebra over U and n ≥ 1 be a natural number. By an nargument rough relation over U we mean any generalized rough set consisting of tuples of the Cartesian product U n . By a rough relational structure we mean U, r 1 , . . . , r k where for 1 ≤ i ≤ k, r i is an n i -argument rough relation over U. One-argument rough relations are called rough concepts and two-argument ones are called rough roles.

The semantics of rough formulas is defined below, where A(x←a) denotes the formula obtained from A by substituting all free occurrences of variable x in A by constant a.

Definition 9 (Semantics of rough formulas). Let U be a set, K = K, ∪, ∩, −, ⊥, be a rough Kleene algebra over U and R = U, r 1 , . . . , r k be a rough relational structure, 1. The value of a rough formula, vs R : KF −→ K, is inductively defined by:

-for a relation symbol r, vs R (r) 

are Kleene formulas with k free variables, and ≤ is the reflexive closure of (3);

where the semantics of ¬, ∨, ∧ on truth values is defined by (4)- (5);

We write R |= A to indicate that v R (A) = T. We say that formulas A and B are equivalent, iff for every R, v R (A) = v R (B).

In the rest of the paper, we assume that knowledge bases are given in the form of finitely axiomatizable theories. As indicated in Definition 6, each theory consisting of a finite set of axioms is understood as a single formula, being the conjunction of the axioms.

The following definition, theorem and example have been formulated in [18] . In the rest of the paper T (r←X) denotes the formula resulting from T (r) by replacing every occurrence of r in T by X.

Example 1. Let T ≡ (student(joe) ∨ student(john)) ∧ teacher (john) . Note that:

(student(joe) ∨ student(john)) ∧ teacher (john) student←X = (X(joe) ∨ X(john)) ∧ teacher (john).

Using Theorem 1 and (7) we have:

forget(T ; student) = ∃X (X(joe) ∨ X(john)) ∧ teacher (john) .

It can be easily shown that the formula ∃X (X(joe)∨X(john))∧teacher (john) , thus forget(T ; student) too, is equivalent to teacher(john).

Theorem 1 shows that the problem of computing forget(T ; r) can be reduced to second-order quantifier elimination. For this purpose, in the current paper we will adapt the techniques of [1, 20] to rough theories. 4

Rough forgetting is defined by analogy with Definition 10.

Let r be a relation symbol and R 1 , R 2 be rough relational structures. Then R 1 ≈ r R 2 denotes the fact that R 1 differs from R 2 at most in the interpretation of r.

Let T be a rough theory. A theory T is a result of rough forgetting r in T iff for any rough relational structure R , R |= T iff there is a rough relational structure R such that R |= T and R ≈ r R . By rforget(T ; r) we denote the formula being the result of rough forgetting of r in T .

As in the case of classical forgetting, we have the following theorem analogous to Theorem 1, where we use a second-order quantifier, whose semantics is defined by:

where max, min are the maximum and minimum wrt (3).

Let r be a rough relation symbol and X be a second-order variable with the same number of arguments as r. Then for every rough relational structure R:

Comparing to classical forgetting, in rough forgetting we deal with rough relations rather than with the classical relations. Thus, ∃X in Theorem 2 is a second-order quantification over rough sets rather than over the classical ones.

To formalize second-order quantifier elimination methods and related concepts, we need a notation A(X←B[z]) defined as follows. Let A, B be rough formulas such that A contains an n-argument second-order variable X andz is a tuple of n first-order variables with free occurrences in formula B. Then:

denotes the result of substituting all occurrences of the second-order variable X by B(z), wherez in B is respectively substituted by actual parameters of X (possibly different in different occurrences of X). For example,

A(X)

[z] is (r(a, y) ∨ r(b, y)).

The quantifier elimination techniques we develop are based on a monotonicity property, defined as follows.

is monotone in X iff for every rough relational structure R and rough formulas B, C not containing X and withz being all variables with free occurrences, one of the following properties holds:

Properties (10) and (11) are called up-monotonicity and down-monotonicity of A, respectively.

The following theorem adapts Ackermann's Lemma [1, 9, 13 ] to rough theories.

Theorem 3. Let X be an n-argument second-order variable. Letz be an ntuple of variables, A(z) be a rough formula containing no occurrences of X, with variablesz occurring free, and let B(X) be a rough formula with X as a free variable.

R, v R ∃X ∀z(A(z) ⊆ X(z)) ∧ B(X) = v R B X←A[z] .(12)

Proof. Let us prove (12) . 6 Let R be an arbitrary rough relational structure. We have to prove three equivalences v R (lhs) = τ iff v R (rhs) = τ for τ ∈ {T, U, F}, where lhs and rhs are respectively the letfthand and the righthand side of Equation (12):

there is X such that v R ∀z(A(z) ⊆ X(z)) = T and v R B(X) = T. Thus, by Definition 9, for everyz, v R A(z) ≤ v R X(z) . By down-monotonicity of

there is X such that v R ∀z(A(z) ⊆ X(z)) = T and B(X) = U. Thus, by Definition 9, for everyz, v R A(z) ≤ v R X(z) . By down-monotonicity of

However, by 1. (←) , (14) implies v R ∃X ∀z(A(z) ⊆ X(z)) ∧ B(X) = T, contradicting the assumption. Therefore, v R B X←A(z)[z] = U.

(←) Here, like in the previous point, it suffices to set ∀z X(z) def = A(z) . 6 The proof of (13) is analogous, so we skip it here. 7 Note that ⊆ is two-valued, i.e., its truth value can only be T or F.

can neither be T nor U (since, as before, this would contradict the assumption). Therefore we can only con-

Here, like in the previous points, it suffices to set ∀z X(z)

The following theorem adapts the fixpoint theorem proved in [20] to rough theories, where Lfp X A(X) and Gfp X A(X) stand for the least and the greatest fixpoint of A(X) wrt X. Note that we deal with complete lattices and will always make sure that A(X) is up-monotone in X, such fixpoints exist by Knaster and Tarski fixpoint theorem.

A(X,z) be up-monotone in X and let B(X) be a rough formula with X being a free variable.

R, v R ∃X ∀z(A(X,z) ⊆ X(z)) ∧ B(X) = v R B X←Lfp X A(X,z)[z] .(15)

Proof. (Sketch) The proof is similar to the proof of Theorem 3. In the case of (15) it suffices to notice that the least X satisfying the lefthand side of the equality is defined by the least fixpoint of A(X). In the case of (16) the suitable X is defined by the greatest fixpoint of A(X). The following lemma shows monotonicity properties of connectives, useful in second-order quantifier elimination. It directly follows from Definition 9. Lemma 1.

Below we will use the following notation: -x, y are variables denoting places and p 1 , . . . , p n are constants denoting places; -ice(x) stands for "x being covered by ice", rain(x) -for "rain in x", freezing(x) -for "temperature in x being close to 0 o C", safe(x) -for "x being safe" and base(x) indicating that "there is a base in place x"; -connected (x, y) stands for "places x, y being (directly) connected", slippery(x, y) -for "connection from x to y being slippery", and sconnected (x, y) -for "x, y being safely connected" (perhaps indirectly, via a chain of connections connected ()).

Let us consider a scenario formalized by the following theory T :

Note that the relations used in (17) 

Remark 4. It is important to note that the conjunction of rough facts, as specified by (23)-(26), does not affect the applicability of the second-order quantifier elimination techniques provided by Theorems 3 and 4.

In the first example, let us forget ice() in the scenario theory above. That is, we consider rforget(T ; ice()) and, according to Theorem 2, we eliminate ∃X from formula:

corresponding to (22) ∧ ∀x∀y (X(x) ∨ X(y)) ⊆ slippery(x, y) corresponding to (17) ∧ B ,

where B def = (18)∧(19)∧(20)∧ (21) . According to Lemma 1, the part of (27) corresponding to (17) is down-monotone in X thus, using equality (12) of Theorem 3, we obtain the following formula equivalent to (27) :

In the second example, let us forget base() in the scenario theory above. We consider rforget(T ; base()) and apply Theorem 2 to eliminate ∃X from:

corresponding to (20) ∧ ∀x safe(x) ⊆ X(x) ∨ ∃y(sconnected (x, y) ∧ X(y)) corresponding to (21) ∧ C ,

where C def = (17)∧(18)∧(19)∧ (22) . According to Lemma 1, the part of (28) corresponding to (21) is up-monotone in X thus, using equality (13) of Theorem 3, the equivalent of (28) is ∀x safe(x) ⊆ safe(x)∨∃y(sconnected (x, y)∧safe(y)) .

Observe that the resulting formula is equivalent to T, so rforget(T ; base()) is equivalent to C. Indeed, when base() is forgotten, the theory no longer provides useful information about safe(), too.

Forgetting rough relations with more than one argument is very similar to forgetting rough concepts. To illustrate the use of Theorem 4, let us forget connected (). That is, consider rforget(T ; connected ()) and, according to Theorem 2, we eliminate ∃X from:

∃X ∀x∀y (x = y ∨ X(y, x)) ⊆ X(x, y) corresponding to (18) ∧ ∀x∀y (X(x, y) ∧ ¬slippery(x, y)) ∨ corresponding to (19) , line 1 (29) ∃z(sconnected (x, z) ∧ sconnected (z, y)) ⊆ sconnected (x, y) (19) According to Lemma 1, the part of (29) corresponding to (19) is down-monotone in X thus, using equality (15) of Theorem 4, we obtain the following equivalent of (29): ∀x∀y (Lfp X(x, y) x = y ∨ X(y, x) (x, y) ∧ ¬slippery(x, y))∨ ∃z(sconnected (x, z) ∧ sconnected (z, y)) ⊆ sconnected (x, y) ∧ D.

Note that Lfp . . . in (30) is equivalent to x = y, so (30) can further be simplified to:

∀x∀y (x = y ∧ ¬slippery(x, y))∨ ∃z(sconnected (x, z) ∧ sconnected (z, y)) ⊆ sconnected (x, y) ∧ D.

In this paper, we provided basic foundations for the specification and application of a forgetting operator for rough theories. To do this, we defined a logical language for rough theories consisting of rough formulas and a semantics for such formulas containing rough relations, in terms of rough Kleene algebras. Using intuitions from work with forgetting operators in classical logic, we then specified a rough forgetting operator in the context of rough relational theories. We then showed how the constructive generation of the result of applying a forgetting operator to a rough theory could be achieved by using second-order quantifier elimination techniques. These foundations open up opportunities for the use of these rough logics for KRR applications and the study of additional types of forgetting operators in this context, in particular of forgetting in rule languages that use a Kleene logic-based semantics. Also, algorithmic techniques based on insights using second-order quantifier elimination techniques, are worth investigating as a basis for forgetting operators used with rough relational theories.

Untersuchungenüber das eliminationsproblem der mathematischen logik

An Investigation of The Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities

Orthopairs: a simple and widely used way to model uncertainty. Fundam

Three-valued logics, uncertainty management and rough sets

A comprehensive study of fuzzy covering-based rough set models: definitions, properties and interrelationships

ABox abduction via forgetting in ALC

Incomplete Information: Structure, Inference

Knowledge Representation Techniques. A Rough Set Approach

Computing circumscription revisited

Computing strongest necessary and weakest sufficient conditions of first-order formulas

On the correspondence between approximations and similarity

A brief survey on forgetting from a knowledge representation and reasoning perspective

Second-Order Quantifier Elimination. Foundations, Computational Aspects and Applications

Uncertainty in big data analytics: survey, opportunities, and challenges

Reasoning about covering-based rough sets using three truth values

Kleene algebras and logic: Boolean and rough set representations, 3-valued, rough set and Perp semantics

On strongest necessary and weakest sufficient conditions

Forget it! In: Proceedings of the AAAI Fall Symposium on Relevance

Rough Sets and Intelligent Systems -Professor Zdzis law Pawlak in Memoriam

A fixpoint approach to second-order quantifier elimination with applications to correspondence theory

Information systems -theoretical foundations

Rough Sets. Theoretical Aspects of Reasoning about Data

Rough Sets. Mathematical Foundations

Tolerance approximation spaces

A generalized definition of rough approximations based on similarity

Forgetting for answer set programs revisited

Forgetting and unfolding for existential rules

Literal projection for first-order logic

A review of rough set models

A survey on rough set theory and its applications

FAME(Q): an automated tool for forgetting in description logics with qualified number restrictions

The first author has been supported by the ELLIIT Network Organization for Information and Communication Technology, Sweden; the Swedish Foundation for Strategic Research SSF (SymbiKBot Project); and a guest professor grant from Jinan University (Zhuhai Campus). The second author has been supported by grant 2017/27/B/ST6/02018 of the National Science Centre Poland.