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

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

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.