遗忘后的公共等价和大小
Common equivalence and size after forgetting
摘要：
忘记命题公式中的变量可能会增加它的大小。引入新的变量是缩短它的一种方法，这两种操作都可以用公共等价来表示，等价的弱化版本。反过来，共同的对等可以用遗忘来表达。给出了Horn情形下多项式空间中公共等价的遗忘和检验算法，对于单头公式子类，该算法是多项式时间的。如果公式也是非循环的，并且变量不能被引入，则在遗忘后最小化是多项式时间的，当变量可以被引入时是NP难的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
