重构单头公式以促进逻辑遗忘
Reconstructing a single-head formula to facilitate logical forgetting
摘要：
逻辑遗忘通常需要指数时间，但当它的输入是一个单头命题确定的Horn公式时，它不会。单头意味着没有变量是多个子句的头。给出了一种使公式在可能的情况下成为单头公式的算法。它比前一个更完善：它总是找到一个等价于给定公式的单头公式（如果有的话）。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
