A New Method of Discovering Mathematical Proofs

Overview

The purpose of this project is to create a new method of automated theorem proving for first-order logic. The method is a template for computer programs that attempt to prove theorems. The project focuses on using mathematics to analyze the correctness and efficiency of the method rather than creating actual computer programs. The new method is a modification of the method of general matings. The method of general matings searches for a successful proof within a search space made up of ready-made possible proofs. The search-oriented view of the method is enhanced in two ways. First, it is shown how to check possible proofs for success by using fast existing computer programs called SAT solvers. Second, it is shown how to use guided search instead of brute-force search. The method of general matings cannot reason about equations; however, many theorems involve equations. The new method is extended to reason about equations. The equation reasoning capability is designed to be identical to the equation-less method when proving theorems that do not involve equations. It is shown how to check possible proofs for success by using fast existing computer programs called SAT solvers and SMT solvers. It is shown how to use guided search instead of brute-force search. The theoretical efficiencies of the equation-less method are analyzed. The general version of the equation-less method is competitive with existing methods on a certain type of problem called a rigid problem. One specific algorithm based on the method is developed. However, it is shown that the algorithm may require a factorial number of calls to a SAT solver. This means that it is inefficient.

Competition history

• ISEF 2014 Materials Science · Entry MA042

Resources

• ISEF abstract page ↗

Related projects

Closest projects by meaning, across every fair and year in the corpus.