提取已验证的决策过程：DPLL和Resolution
Extracting verified decision procedures: DPLL and Resolution
摘要：
本文研究程序抽取技术在一类新的问题中的应用：构造正确的经典可满足性问题的决策过程的综合。为此，我们形式化的DPLL证明系统的完整性证明，并提取SAT solver.When应用于一个命题公式在合取范式的程序产生一个令人满意的分配或DPLL推导显示其不可满足性。我们使用非计算性量词从提取的程序中删除冗余的计算内容，并将其转换为Haskell以提高性能。我们还证明了分辨率证明系统和DPLL证明系统之间的等价性，并对所得到的分辨率证明的大小进行了限制。这表明可以在证明级别上捕获关于所提取程序的定量信息。在交互式证明助手Minlog中进行形式化。
英文摘要：
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
