Automated Theory Formation Applied to Four Learning Tasks

Automated theory formation involves, amongst other things, the production of examples, concepts and statements relating the concepts. The HR program has been developed to form theories in mathematical domains, by calculating examples, inventing concepts, making conjectures, and settling conjectures using the Otter theorem prover and MACE model generator. In addition to providing a plausible model for automated theory formation in pure mathematics, HR has been applied to other problems in Artificial Intelligence. We discuss HR's application to inducing definitions from examples, scientific discovery, problem solving and puzzle generation. For each problem, we look at how a theory formation approach can be applied and mention some initial results from the application of HR. Our aim is not to describe the applications in great detail, but rather to provide an overview of how HR is used for these problems. This will facilitate a comparison of the problems and discussion of the effectiveness of theory formation for these tasks. Our second aim is to compare HR with the Progol machine learning program. We do this first by looking at the concept formation these programs perform. Also, by suggesting how Progol could be used for the applications mentioned above, we compare the programs in terms of how they can be applied