Dual Forgetting Operators in the Context of Weakest Sufficient and Strongest Necessary Conditions

要約

忘却は、知識表現と自動推論における重要な概念であり、多くの分野にわたって広く応用されている。標準的な忘却演算子は、[Lin and Reiter’94]でモデル理論的意味論の観点から特徴づけられ、主に命題の場合に焦点を当て、新しい研究サブエリアを開いたものである。本論文では、標準忘却と対になる弱忘却と呼ばれる新しい演算子を導入し、両者を合わせて、忘却演算子一般について、より統一的な新しい視点を提供することを示すものである。弱忘却と標準忘却の両演算子は、モデル理論的な意味論ではなく、含意と推論の観点から特徴づけられる。これは当然、量化子の消去とAckermmanのLemmaとそのfixpointの一般化の使用に基づく有用なアルゴリズム的視点につながる。標準的な忘却と最強の必要条件、弱い忘却と最弱の十分条件の間の強い形式的関係も、使用される含意ベースの推論的視点によって極めて自然に特徴付けられる。また、二重の忘却演算子を特徴づけるために使用されるフレームワークは、一階ケースに一般化され、特殊なケースで一階忘却演算子を計算するための有用なアルゴリズムが含まれています。また、モデル化と表現における弱い忘却と標準的な忘却の両方の重要性を示すために、実用的な例も含まれている。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL