论分离关系逻辑的表意能力
计算机科学中的逻辑
2022-08-03 v1
摘要
我们比较了在无限制关系签名上的分离逻辑存在片段（SLR）——仅以分离合取为逻辑连接词并带高阶归纳定义，传统上称为符号堆片段——与（一元）二阶逻辑（(M)SO）的模型论表意能力。尽管 SLR 与 MSO 在树宽无界的结构上不可比较，但结果表明 SLR 一般可嵌入 SO 中，而当模型的树宽由给定输入参数界定时，MSO 成为 SLR 的真子集。我们还讨论了定义一个 SLR 片段的问题，该片段在树宽有界模型上与 MSO 等价。这样的片段将成为最具一般性的、具有可判定蕴含问题的分离逻辑，而可判定蕴含问题是面向自适应（可重构）基于组件与分布式系统的实用验证方法的关键要素。
引用
@article{arxiv.2208.01520,
title = {On the Expressiveness of a Logic of Separated Relations},
author = {Radu Iosif and Florian Zuleger},
journal= {arXiv preprint arXiv:2208.01520},
year = {2022}
}