角色逻辑中的广义记录与空间合取
On Generalized Records and Spatial Conjunction in Role Logic
摘要：
我们以前已经介绍了角色逻辑作为一种符号，用于描述形状分析，数据库和知识库中的关系结构的属性。角色逻辑的自然片段对应于具有计数的二元逻辑，因此是可判定的。我们展示了如何使用角色逻辑来描述打开和关闭的记录，以及记录的对偶，反向记录。我们观察到分离逻辑的空间合取操作自然地模拟记录连接。此外，我们还讨论了如何用计数消除一阶逻辑中量词深度为1的公式的空间合取。因此，允许量词深度1的公式的空间合取保持了具有计数的二元逻辑的可判定性。这一结果同样适用于双变量角色逻辑片段。由此产生的逻辑顺利地集成了类型系统和谓词演算符号，可以被看作是一个自然的概括符号的约束中出现的角色分析和类似的形状分析方法。
英文摘要：
We have previously introduced role logic as a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-variable logic with counting and is therefore decidable. We show how to use role logic to describe open and closed records, as well the dual of records, inverse records. We observe that the spatial conjunction operation of separation logic naturally models record concatenation. Moreover, we show how to eliminate the spatial conjunction of formulas of quantifier depth one in first-order logic with counting. As a result, allowing spatial conjunction of formulas of quantifier depth one preserves the decidability of two-variable logic with counting. This result applies to two-variable role logic fragment as well. The resulting logic smoothly integrates type system and predicate calculus notation and can be viewed as a natural generalization of the notation for constraints arising in role analysis and similar shape analysis approaches.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
