SHF: Small: Synergy between Automated Reasoning and Interactive Theorem Proving

SHF：小：自动推理和交互式定理证明之间的协同作用

• 批准号: 2229099
• 负责人: Marienus Heule
• 金额: $ 54.4万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2229099&HistoricalAwards=false
• 关键词: SHF; Small; Synergy; between; Automated

Automated reasoning systems are used to solve complex problems in mathematics and computer science. The method involves translating problems into a fundamental logical language. For efficiency, very subtle translations are often used. It is then hard to be sure that the translation adequately represents the original problem and that the automated reasoning results therefore have the intended meaning. The novelty of this project is the use of a mathematical verification system based on logic, to check the correctness of translations. The projects' impacts include having more flexible and reliable means of solving hard problems in mathematics and computer science using automated reasoning technology.Specifically, this project aims to develop formal libraries, methods, and tools for carrying out all of the following tasks in verified ways:encoding statements as clausal formulas; using results from satisfiability (SAT) solvers to justify further reductions; reducing search space by introducing clauses that break symmetry; and carrying out substantial transformations of problems to reduce them to forms amenable to verification by SAT solvers. The project uses the Lean interactive proof assistant to verify correctness, and demonstrates the utility of its methods by applying them to notable problems in mathematics and computer science.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

自动推理系统用于解决数学和计算机科学中的复杂问题。该方法涉及将问题翻译成基本的逻辑语言。为了提高效率，经常使用非常微妙的翻译。然后很难确定翻译是否充分代表了原始问题，并且自动推理结果因此具有预期含义。该项目的新颖之处在于使用基于逻辑的数学验证系统来检查翻译的正确性。该项目的影响包括使用自动推理技术解决数学和计算机科学中的难题有更灵活和可靠的方法。具体来说，该项目旨在开发正式的库、方法和工具，以经过验证的方式执行以下所有任务：将语句编码为子句公式；使用可满足性 (SAT) 求解器的结果来证明进一步减少的合理性；通过引入破坏对称性的子句来减少搜索空间；对问题进行实质性转换，将其简化为 SAT 求解器可以验证的形式。该项目使用精益交互式证明助手来验证正确性，并通过将其应用于数学和计算机科学中的显着问题来展示其方法的实用性。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力评估进行评估，认为值得支持。优点和更广泛的影响审查标准。

项目成果

Verified Encodings for SAT Solvers

SAT 求解器的验证编码

• 发表时间: 2023
• 期刊: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023
• 作者: Codel, Cayden;Avigad, Jeremy;Heule, Marijn J.
• 通讯作者: Heule, Marijn J.

Propositional Proof Skeletons

命题证明骨架

• 发表时间: 2023
• 期刊: Springer
• 作者: Reeves, Joseph E.;Kiesl-Reiter, Benjamin;Heule, Marijn J.
• 通讯作者: Heule, Marijn J.