• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of symbolic computation >Combination of convex theories: Modularity, deduction completeness, and explanation
【24h】

Combination of convex theories: Modularity, deduction completeness, and explanation

机译：凸理论的组合：模块化，演绎完整性和解释性

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

摘要

Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple "sat/unsat" answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.
机译：决策程序是定理证明和约束满足系统的关键组成部分。它们的模块化组合是构建高效系统的主要兴趣，但是当此类过程仅提供简单的“ sat / unsat”答案时，它们的有效使用通常会受到不良的接口功能的限制。在本文中，我们开发了一个框架来设计此类过程之间的协作模式，同时保持其接口的模块化。首先，我们使用该框架来指定和证明Nelson-Oppen和Shostak的经典组合方案的正确性。其次，我们介绍了演绎完整可满足性过程的概念，展示了如何针对大型理论类构建它们，然后提供了将它们模块化组合的方案。第三，我们考虑通过对组件理论重新使用可用的证明生成程序来模块化构造组合说明的问题。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号