[Submitted on 8 May 2020]
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$. The hardness results employ superredundancy: a
superirredundant clause is in all formulae of minimal size equivalent to a
given one. This concept may be useful outside forgetting.
Submission history
From: Paolo Liberatore [view email]
[v1]
Fri, 8 May 2020 15:56:01 UTC (75 KB)
