IL: An artificial intelligence approach to theory formation in mathematics.

摘要

This dissertation addresses the problem of building a computer program which can reason realistically in a complex mathematical domain. Computer programs have been built which model various elements of mathematical reasoning. For example, automatic theorem provers have been extensively studied over the last few decades. On the other hand, there have only been a few programs which have addressed the holistic elements of reasoning in mathematics, most notably Lenat's AM system and Epstein's GT system. Since these systems appear capable of independent discovery of concepts and properties, they are referred to as mathematical discovery systems. Previous mathematical discovery systems have been inadequate in two related ways: (i) they were not capable of easily representing new areas of mathematics, since the representations of concepts were tightly tuned to the applications investigated, and (ii) they lacked the ability to reason deductively. In order to address these limitations, I developed a computer program, called IL, which has the following distinguishing features: (1) it synergistically couples empirical investigations with deduction and (2) it declaratively represents mathematical concepts. I have applied IL to the mathematical domain of Conway or Surreal numbers, where IL has (re)discovered the Conway additive identity property, some elementary theorems, and the definition of Conway multiplication.