Terminating Tableau Systems for Hybrid Logic with Difference and Converse
Terminating Tableau Systems for Hybrid Logic with Difference and Converse
复制标题
使用 Difference 和 Converse 终止混合逻辑的 Tableau 系统
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
G. Smolka
中科院分区：
文献类型：
--
作者：
M. Kaminski;G. Smolka
本文有助于原则性的建设表为基础的决策程序的混合逻辑与全球，差异，匡威模态。我们还考虑了自反和传递关系。对于反向自由公式，我们提出了一个终止控制，不依赖于通常的基于链的阻塞计划。我们的表系统是基于一个新的模型存在定理。
This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence theorem.