Copenhagen Winter School on Abstract Software Specifications**, D. Bjørner, Ed. Lecture** Notes in Computer Science, vol. 86. Springer, 43–99.

Wang, K., Wang, Z., Topor, R. W., Pan, J. Z., and Antoniou, G. **2009. Concept**
and role forgetting in ALC ontologies. In **Proceedings of the 8th International Semantic**
Web Conference (ISWC 2009)**, A. Bernstein, D. R. Karger, T. Heath, L. Feigenbaum,** D. Maynard, E. Motta, and K. Thirunarayan, Eds. Lecture Notes in Computer Science, vol. 5823. Springer, Chantilly, VA, USA, 666–681.

Winslett, M. 1988. Reasoning about action using a possible models approach. In Proceedings of the 7th National Conference on Artificial Intelligence (AAAI 1988)**. AAAI**
Press / The MIT Press, Saint Paul, MN, USA, 89–93.

Winslett, M. 1990. Updating Logical Databases**. Cambridge University Press, New York,**
NY, USA.

Zhang, Y. and Foo, N. Y. 2005. A unified framework for representing logic program updates. In **Proceedings of the 20th National Conference on Artificial Intelligence (AAAI**
2005)**, M. M. Veloso and S. Kambhampati, Eds. AAAI Press / The MIT Press, Pittsburgh, Pennsylvania, USA, 707–713.**

## Appendix A Kleene Fixed Point Theorem

Fixed points play an important role in many of the investigations in the area of logic programming. Many semantics of logic programs are defined by a **fixed point**
equation, meaning that in order for an interpretation M **to be considered a "good"** model of a logic program, it must satisfy some equation of the form M = f(M)
where f is a mapping from interpretations to interpretations, also called an operator**. Such operators were heavily studied in Order Theory and Kleene Fixed Point**
Theorem is one of its basic results. Informally, it states that the least fixed point of a continuous operator can be computed by iterating the operator. It is heavily used in logic programming.

For the sake of self-containedness, this Appendix introduces the **basic notions**
of Order Theory necessary to formally state and prove the Kleene **Fixed Point** Theorem. For an elaborate study of this topic with many further references, we refer the reader to (Davey and Priestley 1990).

The first definition is of a partially ordered set, under which we mean any set with an associated relation "≤**" that can be used to compare elements of this set.**
This relation is required to obey certain properties that can be naturally expected from any such ordering relation. Definition A.1 (**Partial Order** ) A partial order is a pair (P, ≤) where P is a set and ≤ **is a reflexive, antisymetric and** transitive relation over P, i.e. the following conditions are satisfied for all **a, b, c** ∈ P:
a ≤ a
(a ≤ b ∧ b ≤ a) ⇒ a = b
(a ≤ b ∧ b ≤ c) ⇒ a ≤ c