Discoveries and experiments in the automation of mathematical reasoning

The problem of automatically proving that a statement follows logically from a base of knowledge is recurrent in artificial intelligence and automated theorem proving research. It is a problem that mathematicians must handle very well in order to prove theorems in mathematics. One of the difficulties of proving a statement is choosing when and how to use the knowledge one has about the topic. Since this is difficult for mathematicians, we can expect that it will be difficult for machines.;In this dissertation, the author describes a framework for approaching this problem and illustrates its success on certain kinds of problems. A simple and tractable calculus is also described for handling parts of set theory and equality. These devices allow for more complicated mathematical expressions and theories to be handled more easily.;The rules presented here for storing and applying knowledge were designed with the aim of facilitating human interface. Knowledge is stored in a format that is much more cognitively sensible than the standard clausal form. Knowledge is applied during the search for a proof in a way that is very similar to the way humans explain the application of knowledge in proofs.;The computer program, IPR, uses the advantages of the framework not only to find proofs of statements in theories under difficult circumstances but also to provide features that make it easy to be used by someone who knows nothing about automated methods but who wants to get directly into mathematical reasoning. The method is very easy to implement and facilitates excellent interactive capabilities including help for the user in understanding an unfinished proof.