论文标题
重建单头公式以促进逻辑遗忘
Reconstructing a single-head formula to facilitate logical forgetting
论文作者
论文摘要
逻辑上的遗忘通常可能需要指数时间，但是当它的输入是单头命题确定的角公式时，它并不是。单头意味着没有变量是多个子句的头部。显示出一种以单头为单位的算法。它通过完成来改善上一个：它总是发现单头公式等于给定的公式。
Logical forgetting may take exponential time in general, but it does not when its input is a single-head propositional definite Horn formula. Single-head means that no variable is the head of multiple clauses. An algorithm to make a formula single-head if possible is shown. It improves over a previous one by being complete: it always finds a single-head formula equivalent to the given one if any.
