• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer Science Logic >Resource Tableaux
【24h】

Resource Tableaux

机译：资源表

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a "pointer logic" semantics for programs which 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, ⊥, 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. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI's pointer logic and for which BI is complete
机译：聚类含义的逻辑BI提供了对资源丰富的基本概念的逻辑分析，该概念足够丰富，可以为处理可变数据结构的程序提供“指针逻辑”语义。我们为BI开发了语义表理论，因此为BI的有效定理证明工具提供了优雅的基础。它基于为BI的表格使用标签代数来解决资源分配问题，标签是资源模型的要素。对于不一致的BI，挑战在于在这种基于标签的证明搜索方法中处理BI的Grothendieck拓扑模型。我们针对这种语义证明了资源表方法TBI的健全性和完整性定理，并提供了一种从所谓的依赖图构建对等模型的方法。结果，对于BI，我们有两个重要的新结果：命题BI的可判定性和关于Grothendieck拓扑语义的有限模型属性。另外，通过考虑部分定义的等分线，我们提出了一种新的语义，该语义泛化了BI指针逻辑的语义，并且BI已完成

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号