• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >BDI: a new decidable clause class
【24h】

BDI: a new decidable clause class

机译：BDI：新的可判定子句类

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

摘要

BDI (Bounded Depth Increase) is a new decidable first-order clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of 'cycles' in resolution inferences is restricted so that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real-world problems where function terms are used to represent record structures. We show that the hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure.
机译：BDI（边界深度增加）是一个新的可确定的一阶子句类。它严格包含已知类，例如PVD。在BDI中，功能和谓词符号的多样性以及原子的形状不受限制。相反，解析推理中“循环”的形状受到限制，因此生成子句的深度可能会增加，但仍然受到限制。 BDI类是由现实世界中的问题激发的，在现实世界中，功能项用于表示记录结构。我们表明，超分辨率演算的模数冗余消除在BDI子句集上终止。通过将此结果用于有序分辨率演算，我们还可以证明BDI上有序分辨率的终止，从而产生更有效的决策程序。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号