• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>urnal of Symbolic Computation >Constraint contextual rewriting
【24h】

Constraint contextual rewriting

机译：约束上下文重写

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

摘要

The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. In this paper we address the problem by proposing a general pattern of interaction between rewriting and decision procedures and by providing an account of such a pattern of interaction which is precise and concise at the same time. The first step amounts to a generalization of contextual rewriting which allows the available decision procedure to access and manipulate the rewriting context. We call this generalized form of contextual rewriting constraint contextual rewriting (CCR for short). The second step amounts to providing a rule-based presentation of CCR which is modular, declarative, and formal at the same time. This allows us to give a rigorous account of CCR and to formally state and prove its soundness and termination.
机译：决策程序在公式简化中的有效集成是机械验证中的一个基本问题。在本文中，我们通过提出重写和决策过程之间的通用交互模式并提供这种精确而简洁的交互模式的说明来解决该问题。第一步就是上下文重写的一般化，它允许可用的决策过程访问和操纵重写上下文。我们称这种形式的上下文重写约束是上下文重写（简称CCR）。第二步相当于提供基于规则的CCR表示，它同时是模块化，声明性和正式的。这使我们能够对CCR进行严格的说明，并正式陈述和证明其合理性和终止性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号