Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Patrick Doherty, Andrzej Szalas

TL;DR

This paper introduces a dual weakening of the standard forgetting operator, called weak forgetting, and develops an entailment-based framework that treats forgetting as preserving either strongest necessary conditions or weakest sufficient conditions. The authors formalize two operators, $F^{NC}$ and $F^{SC}$, showing that $F^{NC}$ corresponds to preserving necessary-condition entailment and $F^{SC}$ to preserving sufficient-condition entailment; each has a precise second-order characterization and an Ackermann-like quantifier-elimination approach for computation. The work extends to first-order and fixpoint settings, with the DLS and DLS* algorithms adapted for efficient computation, and provides practical examples illustrating when weak forgetting yields richer, more usable results than standard forgetting. By connecting forgetting with strongest/weakest-condition notions, the framework offers a principled, inference-driven way to reason under partial observability and signatures reduction, with implications for knowledge representation, belief revision, and modular reasoning.

Abstract

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.

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

TL;DR

This paper introduces a dual weakening of the standard forgetting operator, called weak forgetting, and develops an entailment-based framework that treats forgetting as preserving either strongest necessary conditions or weakest sufficient conditions. The authors formalize two operators, and , showing that corresponds to preserving necessary-condition entailment and to preserving sufficient-condition entailment; each has a precise second-order characterization and an Ackermann-like quantifier-elimination approach for computation. The work extends to first-order and fixpoint settings, with the DLS and DLS* algorithms adapted for efficient computation, and provides practical examples illustrating when weak forgetting yields richer, more usable results than standard forgetting. By connecting forgetting with strongest/weakest-condition notions, the framework offers a principled, inference-driven way to reason under partial observability and signatures reduction, with implications for knowledge representation, belief revision, and modular reasoning.

Abstract

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.
Paper Structure (26 sections, 10 theorems, 73 equations, 2 figures, 1 algorithm)

This paper contains 26 sections, 10 theorems, 73 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction and Motivation
  2. Preliminaries
  3. Classical Propositional Logic
  4. Standard Forgetting
  5. An Ackermann-Like Approach to Second-Order Quantifier Elimination
  6. The Entailment-Based Inferential Perspective on Forgetting
  7. Some Intuitions
  8. The Operator $F^{NC}()$
  9. The Analysis of the Left-to-Right Direction
  10. The Analysis of the Right-to-Left Direction
  11. A Characterization of $F^{NC}()$
  12. The Operator $F^{SC}()$
  13. The Analysis of the Left-to-Right Direction
  14. The Analysis of the Right-to-Left Direction
  15. A Characterization of $F^{SC}()$
  16. ...and 11 more sections

Key Result

Theorem 2.1

Let $\bar{p}$ and $\bar{q}$ be disjoint tuples of propositional variables, $A$ be a formula not containing occurrences of variables from $\bar{p}$ and $Th(\bar{p},\bar{q})$ be a theory. Then: $\Box$

Figures (2)

  • Figure 1: An illustration of intuitions behind Ackermann-like lemmas.
  • Figure 2: The relationships between forgetting operators and the original theory in terms of entailment: the ovals inclusion indicates that the formula in an inner oval entails the formula in an outer one.

Theorems & Definitions (16)

  • Theorem 2.1: Lin, Reiter
  • Lemma 2.2: Propositional Ackermann Lemma
  • Theorem 3.1
  • Theorem 3.2
  • Example 3.3
  • Example 4.1
  • Example 4.2
  • Example 4.3
  • Lemma 5.1
  • Corollary 5.2
  • ...and 6 more