The semantics of BI and resource tableaux
The semantics of BI and resource tableaux
复制标题
DOI：
10.1017/s0960129505004858
复制
发表时间：
2005-12-01
影响因子：
0.5
通讯作者：
Pym, D
中科院分区：
文献类型：
--
作者：
Galmiche, D;Méry, D;Pym, D
BIND含义的逻辑BI，对资源的基本概念进行了逻辑分析，例如足够丰富的资源概念，例如为操纵可变数据结构的程序形成“指针逻辑”的逻辑基础，并为“指针逻辑”的逻辑依据。我们为BI开发了语义tableaux的理论，因此为有效的理论提供了优雅的基础，以证明BI的工具。它基于将标签代数用于BI的Tableaux来解决资源分布问题，标签是资源模型的元素。对于垂直于持续存在的BI，基于标签的证明搜索方法，挑战在于处理BI的Grothendieck拓扑模型。对于此语义，我们证明了资源tableaux方法TBI的健全性和完整定理，并提供了一种从所谓的依赖图构建反模型的方法。然后，从这些结果中，我们可以基于部分定义的单体定义BI的新资源语义，并证明该语义已完成。这种基于部分性的语义与BI（直觉）指针和分离逻辑的语义密切相关。返回tableaux演算，我们提出了一个具有自由化规则的新版本，该版本与BI的拓扑Kripke语义密切相关。作为BI语义与资源tableaux语义之间关系的后果，我们证明了命题BI的两个新结果：其可决定性和在拓扑语义方面的有限模型属性。
The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource that is rich enough, for example, to form the logical basis for 'pointer logic' and,separation logic' semantics for programs that manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, perpendicular to, the challenge consists in dealing with BI's Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. Then, from these results, we can define a new resource semantics of BI, based on partially defined monoids, and prove that this semantics is complete. Such a semantics, based on partiality, is closely related to the semantics of BI's (intuitionistic) pointer and separation logics. Returning to the tableaux calculus, we propose a new version with liberalised rules for which the countermodels are closely related to the topological Kripke semantics of BI. As consequences of the relationships between semantics of BI and resource tableaux, we prove two new strong results for propositional BI: its decidability and the finite model property with respect to topological semantics.