Forgetting is an important concept in knowledge representation and automated reasoning with widespread applications across a number of disciplines. A standard forgetting operator, characterized in [Lin and Reiter'94] in terms of model-theoretic semantics and primarily focusing on the propositional case, opened up a new research subarea. In this paper, a new operator called weak forgetting, dual to standard forgetting, is introduced and both together are shown to offer a new more uniform perspective on forgetting operators in general. Both the weak and standard forgetting operators are characterized in terms of entailment and inference, rather than a model theoretic semantics. This naturally leads to a useful algorithmic perspective based on quantifier elimination and the use of Ackermman's Lemma and its fixpoint generalization. The strong formal relationship between standard forgetting and strongest necessary conditions and weak forgetting and weakest sufficient conditions is also characterized quite naturally through the entailment-based, inferential perspective used. The framework used to characterize the dual forgetting operators is also generalized to the first-order case and includes useful algorithms for computing first-order forgetting operators in special cases. Practical examples are also included to show the importance of both weak and standard forgetting in modeling and representation.

翻译：遗忘是知识表示与自动推理中的重要概念，在多个学科领域具有广泛应用。由Lin和Reiter于1994年提出的标准遗忘算子（基于模型论语义刻画，主要关注命题逻辑情形）开创了一个新的研究子领域。本文引入了一种称为弱遗忘的新算子（与标准遗忘对偶），并证明两者共同为遗忘算子提供了更统一的视角。不同于模型论语义，弱遗忘与标准遗忘算子均基于蕴涵和推理进行刻画，这自然引出了基于量词消去及阿克曼引理及其不动点推广的有效算法视角。通过基于蕴涵的推理视角，本文还自然刻画了标准遗忘与强必要条件、弱遗忘与弱充分条件之间的强形式关系。用于刻画对偶遗忘算子的框架也被推广到一阶逻辑情形，并包含在特殊情形下计算一阶遗忘算子的实用算法。最后通过实际案例展示了弱遗忘与标准遗忘在建模与表示中的重要性。