论文标题
一个头大于两个：命题确定的角遗忘的多项式限制
One head is better than two: a polynomial restriction for propositional definite Horn forgetting
论文作者
论文摘要
即使在简单的命题号角公式的情况下，逻辑上的遗忘也是\ np的完整，并且可能会指数增加其大小。忘记的一种方法是替换每个变量，用每个子句的正文忘记其头为变量的子句。在单头情况下需要多项式时间：每个变量最多都是子句的头部。某些公式不是单头，但可以简化忘记。它们是单头等效的。本文的第一个贡献是研究单头对等的语义表征。给出了两个必要的条件。当公式不等于时，它们就足够了：仅当它们也等同于它们的相交时，它才能使两组变量相等。所有无环公式都是不相等的。本文的第二个贡献是用于转动公式单头的不完整算法。在成功的情况下，忘记在多项式时间内成为可能，并且会产生多项式大小的公式，否则没有任何保证。该算法在不相等公式上完成。
Logical forgetting is \np-complete even in the simple case of propositional Horn formulae, and may exponentially increase their size. A way to forget is to replace each variable to forget with the body of each clause whose head is the variable. It takes polynomial time in the single-head case: each variable is at most the head of a clause. Some formulae are not single-head but can be made so to simplify forgetting. They are single-head equivalent. The first contribution of this article is the study of a semantical characterization of single-head equivalence. Two necessary conditions are given. They are sufficient when the formula is inequivalent: it makes two sets of variables equivalent only if they are also equivalent to their intersection. All acyclic formulae are inequivalent. The second contribution of this article is an incomplete algorithm for turning a formula single-head. In case of success, forgetting becomes possible in polynomial time and produces a polynomial-size formula, none of which is otherwise guaranteed. The algorithm is complete on inequivalent formulae.
