关于分离关系归纳逻辑的表达能力结果
摘要：关于关系的分离逻辑（SLR）的研究及其与（单调）二阶逻辑（M）SO的表达能力的比较。SLR基于分离逻辑的著名符号堆片段，其公式由指向断言、归纳定义的谓词组成，分隔连接是唯一的逻辑连词。SLR通过支持一般的关系原子，而不仅仅是指向断言，来推广符号堆片段。本文限制自己在有限的关系结构上进行研究，因此只考虑量化范围为有限集合的弱（M）SO。我们的主要结果是，在无限的树宽结构上，SLR和MSO是无法比较的，而SLR通常可以嵌入到SO中。此外，当模型的树宽由参数限制且所有与某个超边相关联的顶点属于一个固定一元关系符号的解释时，MSO成为SLR的真子集。我们还讨论了识别一个与有界树宽模型上的MSO等价的SLR片段的问题。
作者：Radu Iosif, Florian Zuleger
论文ID：2307.02381
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-06