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$.
翻译:忘记了逻辑公式中的变量, 同时又保留了其他变量的限制。 尽管它是一种缩减形式, 它并不总是减少公式的大小, 有时甚至会增加它。 文章讨论了这种增加的影响, 并分析了该现象的计算属性 。 考虑到一个假设的角公式、 一组变量和最大允许大小, 决定该公式中的变量是否可以以该大小表示为$D ⁇ p$- hard $\Sigma ⁇ p_ p_ 2 $ 。 对于无限制的公式来说, 同样的问题就是$D ⁇ p_ 2$- hard $\Sigma_ p_ 3$ 。