• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(LPAR 2005); 20051202-06; Montego Bay(JM) >Bounding Resource Consumption with Godel-Dummett Logics
【24h】

Bounding Resource Consumption with Godel-Dummett Logics

机译：Godel-Dummett Logics限制资源消耗

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Godel-Dummett logic LC and its finite approximations LC_n are the intermediate logics complete w.r.t. linearly ordered Kripke models. In this paper, we use LC_n logics as a tool to bound resource consumption in some process calculi. We introduce a non-deterministic process calculus where the consumption of a particular resource denoted · is explicit and provide an operational semantics which measures the consumption of this resource. We present a linear transformation of a process P into a formula f of LC. We show that the consumption of the resource by P can be bounded by the positive integer n if and only if the formula f admits a counter-model in LCn. Combining this result with our previous results on proof and counter-model construction for LC_n, we conclude that bounding resource consumption is (linearly) equivalent to searching counter-models in LC_n.
机译：Godel-Dummett逻辑LC及其有限逼近LC_n是中间逻辑完整w.r.t.线性排序的Kripke模型。在本文中，我们使用LC_n逻辑作为工具来约束某些过程计算中的资源消耗。我们介绍了一种不确定的过程演算，其中表示为的特定资源的消耗是明确的，并提供了一种可操作的语义，用于测量该资源的消耗。我们提出了将过程P线性转换为LC公式f的过程。我们证明，当且仅当公式f在LCn中允许使用反模型时，P的资源消耗才能由正整数n限制。将该结果与我们先前关于LC_n的证明和反模型构建的结果相结合，我们得出的结论是，有限资源消耗（线性）等效于在LC_n中搜索反模型。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号