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

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

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.