• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>urnal of Symbolic Computation >Deciding the guarded fragments by resolution
【24h】

Deciding the guarded fragments by resolution

机译：通过解析确定受保护的片段

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

摘要

The guarded fragment (GF) is a fragment of first-order logic that has been introduced for two main reasons: first, to explain the good computational and logical behaviour of propositional modal logics. Second, to serve as a breeding ground for well-behaved process logics. In this paper we give resolution-based decision procedures for the GF and for the loosely guarded fragment (LGF) (sometimes also called the pairwise guarded fragment). By constructing an implementable decision procedure for the GF and for the LGF, we obtain an effective procedure for deciding modal logics that can be embedded into these fragments. The procedures have been implemented in the theorem prover Bliksem.
机译：保护性片段（GF）是一阶逻辑的一个片段，由于两个主要原因而被引入：首先，解释命题模态逻辑的良好计算和逻辑行为。第二，充当行为良好的过程逻辑的温床。在本文中，我们为GF和松散保护的片段（LGF）（有时也称为成对保护的片段）提供了基于分辨率的决策程序。通过为GF和LGF构建可行的决策程序，我们获得了一种有效的程序，用于确定可以嵌入这些片段的模态逻辑。该程序已在定理证明者Bliksem中实现。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号