...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >A Proof Theoretic Study of Soft Concurrent Constraint Programming
【24h】

A Proof Theoretic Study of Soft Concurrent Constraint Programming

机译：软并行约束规划的证明理论研究

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

摘要

Concurrent Constraint Programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.
机译：并发约束编程（CCP）是一个简单而强大的并发模型，其中代理通过告知和询问约束进行交互。自成立以来，CCP语言就一直被设计为与逻辑紧密联系。实际上，可以从直觉（线性）逻辑-ILL-的适当片段构建基础约束系统，并且可以将过程解释为ILL中的公式。作为ILL公式的约束无法准确地表示存在“首选项”（称为软约束）（例如概率，不确定性或模糊性）的情况。为了解决这个问题，已经提出了c-半符号作为代数结构，用于定义约束系统，在该系统中允许代理告知和询问软约束。然而，在这种情况下，与逻辑和证明理论的紧密联系丢失了。在这项工作中，我们为软约束提供了理论上的证明：它们可以定义为ILL带有子指数（SELL）的适当片段中的公式，其中以c-半符号结构排序的子指数被解释为首选项。因此，我们实现了两个目标：（1）获得一种CCP语言，在该语言中代理可以说出并询问软约束；（2）证明（1）中的语言与逻辑有很强的联系。因此，我们将声明式的过程作为公式进行阅读，同时为基于软CCP的系统提供逻辑框架。 （1）的一个有趣的副作用是，通过限制将促销规则用于非等幂的c-semiring，人们还能够处理SELL中的概率（和其他方式）。这种控制次指数的更好方法允许考虑更多有趣的空间和限制，并且为指定更具挑战性的计算系统提供了可能性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号