• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>urnal of Symbolic Computation >Hyperresolution for guarded formulae
【24h】

Hyperresolution for guarded formulae

机译：保护公式的超分辨率

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

摘要

This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general, hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragments of the guarded fragment which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1~- and point out several ways of extending this fragment without losing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.
机译：本文研究使用超分辨率作为受保护公式的决策程序和模型构建器。通常，超分辨率不是整个受保护片段的决策过程。但是，我们显示出受保护片段的自然片段可以通过超分辨率来确定。特别地，我们证明了有或没有分裂片段GF1-的超分辨率的可判定性，并指出了在不丧失可判定性的情况下扩展该片段的几种方法。由于超分辨率与各种表格方法密切相关，因此本研究也与表格方法相关。我们比较了使用超平稳的方法，并提到了与其他可通过超分辨率确定的子句类别的关系。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号