论文标题
与算术模态逻辑中的全球假设相结合的推理
Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics
论文作者
论文摘要
我们建立了一个通用的上限限制时间，用于通过全球假设（也称为Tboxes）在煤层模态逻辑中进行推理。与此类结果不同，我们的界限不需要该实例逻辑的一组可行的图表规则，因此结果适用于更广泛的逻辑类别。示例是Presburger模态逻辑，该逻辑扩展了对接班人数量的线性不等式的分级模态逻辑，以及概率模态逻辑，而多项式不平等等于概率。我们使用类型消除算法建立理论上限。我们还提供了一种全球缓存算法，该算法有可能避免构建整个候选国家的指数尺寸空间，从而为实际推理提供了基础。该算法仍然涉及频繁的FIXPOINT计算。我们展示了如何在Liu和Smolka的线性时间固定点算法上模拟的混凝土算法中有效处理这些。最后，我们表明，在逻辑中添加名称，即在煤层杂种逻辑中保留了上层复杂性结合。
We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka's linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e. in coalgebraic hybrid logic.
