Scholarlink

<p>Logical forgetting is NP-complete as a decision problem 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 the head of at most a clause. Some formulae are not single-head but can be made so to simplify forgetting. They are called 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 interequivalent, that is, the formula makes two sets of variables equivalent only if they are also equivalent to their intersection. All acyclic formulae are interequivalent. 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 interequivalent formulae.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

One Head is Better than Two: A Polynomial Restriction for Propositional Definite Horn Forgetting

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年2月9日

查看全文
  • Paolo Liberatore

摘要

Logical forgetting is NP-complete as a decision problem 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 the head of at most a clause. Some formulae are not single-head but can be made so to simplify forgetting. They are called 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 interequivalent, that is, the formula makes two sets of variables equivalent only if they are also equivalent to their intersection. All acyclic formulae are interequivalent. 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 interequivalent formulae.