分离逻辑的石头类型对偶
摘要：Stone型对偶定理是逻辑学中的重要工具，它将代数和关系/拓扑模型联系起来。它不仅具有优雅的抽象性，而且将完备性和一致性的关系加强到范畴等价，从而为代数和拓扑方法提供了一个框架。我们对解释扎堆逻辑的结构的Stone型对偶进行了系统处理，从最弱系统开始，恢复熟悉的BI和布尔型BI（BBI），并扩展到经典的和直观的分离逻辑。我们通过捕获将BI和BBI扩展为与析取、否定和虚假相对应的模态和乘法连接词的扎堆逻辑，展示了这种分析的一致性和模块化。这包括了分离模态逻辑（LSM）、德摩根布尔型BI（DMBI）、经典BI（CBI）以及扩展Bi直觉主义（B）BI（Bi（B）BI）的子经典逻辑系列。我们还获得了在文献中提出的这些逻辑的特定Kripke风格模型的一致性和完备性定理，例如DMBI、扩展BiBI以及一种新的扎堆逻辑——并发Kleene BI（将我们的工作与并发分离逻辑联系起来）。因此，我们在扎堆逻辑环境中得到了所有标准命题连接词的乘法变体的全面语义解释。这种方法综合了模态、次结构和范畴逻辑的各种技术，并将支撑分离逻辑的“资源语义”解释置于其之中。
作者：Simon Docherty and David Pym
论文ID：1710.03021
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22