• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Informatica >Formal Correctness Proof for DPLL Procedure
【24h】

Formal Correctness Proof for DPLL Procedure

机译：DPLL程序的形式正确性证明

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

摘要

The DPLL procedure for the SAT problem is one of the fundamental algorithms in computer science, with many applications in a range of domains, including software and hardware verification. Most of the modern SAT solvers are based on this procedure, extending it with different heuristics. In this paper we present a formal proof that the DPLL procedure is correct. As far as we know, this is the first such proof. The proof was formalized within the Isabelle/Isar proof assistant system. This proof adds to the growing body of formalized mathematical knowledge and it also provides a number of lemmas relevant for proving correctness of modern SAT and SMT solvers.
机译：SAT问题的DPLL程序是计算机科学中的基本算法之一，在包括软件和硬件验证在内的许多领域中都有许多应用。大多数现代SAT求解器都基于此过程，并用不同的启发式方法对其进行了扩展。在本文中，我们提供了DPLL程序正确的正式证明。据我们所知，这是第一个这样的证明。该证明在Isabelle / Isar证明助手系统中正式化。该证明增加了形式化数学知识的增长，也提供了与证明现代SAT和SMT求解器的正确性有关的许多引理。

著录项

  • 来源
    《Informatica》 |2010年第1期|P.57-78|共22页
  • 作者

    Filip MARIC; Predrag JANICIC;

  • 作者单位

    Faculty of Mathematics, University of Belgrade Studentski trg 16, Belgrade, Serbia;

    Faculty of Mathematics, University of Belgrade Studentski trg 16, Belgrade, Serbia;

  • 收录信息 美国《科学引文索引》(SCI);
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

    SAT problem; DPLL procedure; formal proofs; isabelle; isar;

    机译：SAT问题;DPLL程序;正式证明;伊莎贝尔伊萨尔;

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号