The ghosts of forgotten things: A study on size after forgetting

TL;DR

This paper investigates the size implications of the forgetting operation in propositional logic, revealing that size can increase and analyzing the computational complexity of size-bounded forgetting.

Contribution

It provides a formal analysis of size changes during forgetting and establishes the computational hardness of size-restricted forgetting problems.

Findings

Forgetting can increase formula size, not just reduce it.

Deciding size-bounded forgetting is computationally hard ($D^p$-hard).

Complexity varies between Horn and unrestricted formulas.

Abstract

Forgetting is removing variables from a logical formula while preserving the constraints on the other variables. In spite of being a form of reduction, it does not always decrease the size of the formula and may sometimes increase it. This article discusses the implications of such an increase and analyzes the computational properties of the phenomenon. Given a propositional Horn formula, a set of variables and a maximum allowed size, deciding whether forgetting the variables from the formula can be expressed in that size is $D^p$-hard in $\Sigma^p_2$. The same problem for unrestricted propositional formulae is $D^p_2$-hard in $\Sigma^p_3$.