首页> 外文期刊>Journal of logic and computation >Algorithmic correspondence and canonicity for possibility semantics
【24h】

Algorithmic correspondence and canonicity for possibility semantics

机译:用于可能性语义的算法对应关系和Cononicity

获取原文
获取原文并翻译 | 示例

摘要

The present paper develops a unified correspondence treatment of the Sahlqvist theory for possibility semantics, extending the results in the work by Yamamoto (2016, Journal of Logic and Computation, 27, 2411-2430) from Sahlqvist formulas to the strictly larger class of inductive formulas and from the full possibility frames to filter-descriptive possibility frames. Specifically, we define the possibility semantics version of the algorithm Ackermann lemma based algorithm (ALBA) and an adapted interpretation of the expanded modal language used in the algorithm. One notable feature of the adaptation of ALBA to possibility frames setting is that the so-called nominal variables, which are interpreted as complete join-irreducibles in the standard setting, are interpreted as regular open closures of 'singletons' in the present setting, which is a novelty of the present paper. We prove the soundness of the algorithm with respect to both (the dual algebras of) full possibility frames and (the dual algebras of) filter-descriptive possibility frames, use the algorithm to give an alternative proof to the one in the work by Holliday (2016, Possibility frames and forcing for modal logic. UC Berkeley Working Paper in Logic and the Methodology of Science. URL. http://escholarship.org/uc/item/9v11r0dq) that the inductive formulas are constructively canonical and show that the algorithm succeeds on inductive formulas. We make some comparisons among different semantic settings in the design of the algorithms and fit possibility semantics into this broader picture.
机译:本文开发了对萨哈特法理论的统一对应处理的可能性语义,从SAHLQVIST公式到严格更大类别的归纳式诱导公式的山门(逻辑和计算,27,2411-2430)在工作中延长了结果从完整的可能性帧到过滤描述性可能帧。具体而言,我们定义了基于算法Ackermann Lemma的算法(ALBA)的可能性语义版本,以及对算法中使用的扩展模态语言的调整性解释。 Alba适应可能性帧设置的一个值得注意的特征是在标准设置中被解释为完整的加入Irrefigibles的所谓的标称变量,被解释为当前设置中的“单例”的常规打开封闭是本文的新颖性。我们对算法的声音相对于(双代数)的全部可能性帧和(双代数)和(双代数)过滤器描述性可能帧,使用该算法通过Holliday向工作中的一个替代证明( 2016年,可能框架和迫使模态逻辑。UC Berkeley逻辑的工作文件和科学方法。网址http://escholarship.org/uc/Item/9v11r0dq),电感式公式是建设性的规范和表明该算法成功归功于归纳式公式。我们在算法设计中与不同的语义设置进行了一些比较,并将可能性语义设计到了这款更广泛的情况下。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号