• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Checking validity of quantifier-free formulas in combinations of first-order theories.
【24h】

Checking validity of quantifier-free formulas in combinations of first-order theories.

机译：结合一阶理论检查无量词公式的有效性。

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

摘要

An essential component in many verification methods is a fast decision procedure for validating logical expressions. This thesis presents several advances in the theory and implementation of such decision procedures, developed as part of ongoing efforts to improve the Stanford Validity Checker. We begin with the general problem of combining satisfiability procedures for individual theories into a satisfiability procedure for the combined theory. Two known approaches, those of Shostak and Nelson and Oppen, are described. We show how to combine these two methods to obtain the generality of the Nelson-Oppen method while retaining the efficiency of the Shostak method. We then present a general framework for combining decision procedures which includes features for enhancing performance and flexibility. Finally, validity checking requires that a heuristic search be built on top of the core decision procedure for satisfiability. We discuss strategies for efficient heuristic search and show how to adapt several powerful techniques from current research on Boolean satisfiability. Since these algorithms can be extremely subtle, a detailed proof of correctness is provided in the appendix.
机译：许多验证方法的基本组成部分是用于验证逻辑表达式的快速决策过程。本论文介绍了此类决策程序的理论和实施方面的一些进展，这些进展是不断改进斯坦福有效性检查程序的一部分。我们从将单个理论的可满足性过程组合为组合理论的可满足性过程的一般问题开始。描述了两种已知的方法，分别是Shostak和Nelson和Oppen。我们展示了如何结合这两种方法来获得Nelson-Oppen方法的通用性，同时又保留了Shostak方法的效率。然后，我们提出了一个组合决策程序的通用框架，其中包括增强性能和灵活性的功能。最后，有效性检查要求在核心决策过程的基础上进行启发式搜索，以实现可满足性。我们讨论了有效的启发式搜索策略，并展示了如何从布尔可满足性的最新研究中采用几种强大的技术。由于这些算法可能非常微妙，因此附录中提供了正确性的详细证明。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号