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.