• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Completeness and termination for a Seligman-style tableau system
【24h】

Completeness and termination for a Seligman-style tableau system

机译：Seligman样式的Tableau系统的完整性和终止性

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

摘要

Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction and sequent calculus in the 1990s. The purpose of this article is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo, which allows us to 'jump to a named world' on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved by explicit translations that transform tableaus in a standard labelled system into Seligman-style tableaus and vice-versa.
机译：用于混合逻辑的证明系统通常使用@运算符来访问隐藏在模态后面的信息。这种标记方法是最著名的混合分辨率，自然演绎和画面系统的核心。但是还有另一种方法，我们已经认为在概念上更清晰。我们称其为塞利格曼式推论，是杰里·塞利格曼在1990年代首次对自然演绎和后续演算进行介绍和探索的。本文的目的是介绍一种塞利格曼风格的画面系统，以证明其完整性，并说明如何使其终止。 Seligman风格的系统最明显的特征是它们可以使用任意公式，而不仅仅是@ -operators前缀的语句。他们通过引入用于切换到其他证明上下文的机制来做到这一点。通过引入名为GoTo的规则，我们可以在Tableau的设置中捕获此想法，该规则使我们可以在Tableau分支上“跳转到命名世界”。我们首先开发用于基本混合逻辑的Seligman样式的表格系统，并证明其完整性。然后，我们证明了系统的受限制版本的终止而没有求助于循环检查，并证明了限制不会影响完整性。完整性和终止结果均通过将标准标记系统中的表格转换为Seligman样式的表格的显式翻译来证明，反之亦然。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号