论文标题
忘记后的常见等价和大小
Common equivalence and size after forgetting
论文作者
论文摘要
忘记来自命题公式的变量可能会增加其大小。引入新变量是缩短它的一种方式。这两种操作都可以用共同的等效性来表达，这是等价的弱版本。反过来，共同的等价性可以用遗忘来表达。为号角案例提供了一种用于忘记和检查多项式空间中常见等效性的算法；对于单头公式的子类是多项式时间。如果公式也是无环，并且不能引入变量，则忘记后最小化是多项式时间。
Forgetting variables from a propositional formula may increase its size. Introducing new variables is a way to shorten it. Both operations can be expressed in terms of common equivalence, a weakened version of equivalence. In turn, common equivalence can be expressed in terms of forgetting. An algorithm for forgetting and checking common equivalence in polynomial space is given for the Horn case; it is polynomial-time for the subclass of single-head formulae. Minimizing after forgetting is polynomial-time if the formula is also acyclic and variables cannot be introduced, NP-hard when they can.
