• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Boolean unification with predicates
【24h】

Boolean unification with predicates

机译：谓词的布尔统一

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this article, we deal with the following problem which we call Boolean unification with predicates: For a given formula F[X] in first-order logic with equality containing an n-ary predicate variable X, is there a quantifier-free formula G[x1,..., xn] such that the formula F[G] is valid in first-order logic with equality? We obtain the following results. Boolean unification with predicates for quantifier-free F is Pi (P)(2)-complete. In addition, there exists an EXPTIME algorithm which for an input formula F[X], given as above, constructs a formula G such that F[G] being valid in first-order logic with equality, if such a formula exists. For F of the form. root yF'[X, y] with F' quantifier-free, we prove that Boolean unification with predicates is already undecidable. The same holds for F of the form. there exists yF'[X, y] for F'quantifier-free. Instances of Boolean unification with predicates naturally occur in the context of automated theorem proving. Our results are relevant for cut-introduction and the automated search for induction invariants.
机译：在本文中，我们处理以下问题，我们将谓词称为布尔统一：对于一阶逻辑中给定的公式F [X]，其等式包含n元谓词变量X，是否存在无量词公式G [x1，...，xn]这样公式F [G]在具有相等性的一阶逻辑中有效？我们获得以下结果。具有无量词F的谓词的布尔统一是Pi（P）（2）完全。另外，存在EXPTIME算法，该EXPTIME算法对于如上给出的输入公式F [X]，构造公式G，使得F [G]在存在等式的一阶逻辑中有效。对于F的形式。根yF'[X，y]与F'无量词，我们证明谓词的布尔统一已经不可确定。形式的F同样成立。对于无F'量存在yF'[X，y]。布尔与谓词统一的实例自然发生在自动定理证明的背景下。我们的结果与剪切引入和归纳不变量的自动搜索有关。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号