Automated Theory Formation (ATF) is a novel machine learning and discovery approach which has been developed over 15 years, and which is implemented in the HR systems (HR1 in Prolog, HR2 and HR3 in Java). Given some background knowledge, HR forms new concepts from old ones using a set of production rules, and then makes conjectures which relate the concepts, by appealing to empirical patterns in the examples of the concepts. HR then uses third party systems to prove/disprove the conjectures (usually the Otter theorem prover and the MACE model generator). HR also interacts with computer algebra systems such as Maple and Gap, in order to calculate values for concepts. To drive a heuristic search, HR uses a weighted sum - with the weights set by the user - of measures of interestingness for concepts, i.e., having decided which concept is most interesting, HR builds new concepts from this. The book arising from Simon Colton's PhD work is the main reference text for the early work on Automated Theory Formation.

Here are three talks about the HR project, which give an overview of the project and different contexts for it:

The papers below describe how the HR systems have been developed, the applications to which they have been applied and a context in AI for the project.

1. The Development of Automated Theory Formation

The following papers describe some of the fundamental aspects of automated theory formation. The first paper is the main reference for ATF in the HR2 system, described as an Inductive Logic Programming system. The other papers are from quite early on in the development of ATF in the HR1 and HR2 systems.

2. More Sophisticated Mathematical Theory Formation Models

We have taken Automated Theory Formation as the basis for more in-depth studies into how mathematical theories can be formed automatically. In addition to providing extensions to the basic automated theory formation model and providing more background to the subject, these projects have led to more sophisticated systems for mathematical invention and machine learning in general, which take into account philosophical and psychological perspectives on theory formation. The following papers describe some of our projects in this area:

3. The Combination of Reasoning Systems

As described above, the HR system for theory formation routinely appeals to third party software as part of its core routine. This led us to address the more general question of when it is possible to combine AI techniques so that the whole is more than a sum of the parts. In total, we have experimented with various combinations of around 20 different AI systems, including descriptive and predictive machine learning systems, model generators, constraint solvers, satisfiability solvers, theorem provers and computer algebra systems. Many of the applications described below make use of a combination of reasoning systems. We have also looked at some more generic ways to combine AI systems. The following papers describe some of our projects in this area:

4. Applications to Discovery Tasks in Pure Mathematics

Pure mathematics is a unique domain for AI research, as mathematical enquiry involves many diverse forms of reasoning, hence we can look at the question of theory formation in pure mathematics and study computational systems which combine different AI techniques. In addition, the data in pure mathematics is usually error free, hence we can concentrate on pure forms of reasoning without (usually) requiring statistical interpretations. On numerous occasions, we have shown that HR and other systems can make mathematical discoveries of genuine value in graph theory, number theory and various algebraic domains of pure mathematics. In addition, by combining HR with multiple other AI systems, we have achieved new partial classifications of algebraic domains, which were previously beyond any computer (or human). The following papers describe some of our projects in this area:

5. Applications of ATF and Combined Reasoning to Other Domains

While pure mathematics has many advantages, other application domains also stretch the limits of AI systems and their combinations. In order to address the generic nature of the AI systems we have built, we have looked at various non-mathematical applications of ATF. In addition to the projects below, through the supervision of masters projects, we have looked at the usage of HR for musical anomaly detection, for discovery tasks in the gene ontology, for the analysis of board games and the generation of arithmetic puzzles, and for the discovery of software invariants. The following papers describe some of our projects in this area:

6. Improvement of AI Techniques

Given that our overall research goal is to improve the application of AI systems to intelligent tasks, it was sensible for us to question whether combined reasoning systems can improve upon stand-alone systems at standard tasks. Through our experiments with combined reasoning systems, we have shown in many cases that (a) combined reasoning systems can be more flexible in application than stand alone systems (b) combined reasoning systems can be more effective at solving traditional problems than stand alone systems, and (c) combined reasoning systems can undertake intelligent tasks that no single system can attempt. The following papers describe some of our projects in this area: