In recent years, Artificial Intelligence researchers have largely
focused their efforts on solving specific problems, with less emphasis
on 'the big picture' - automating large scale tasks which require
human-level intelligence to undertake. The subject of this book,
automated theory formation in mathematics, is such a large scale task.
Automated theory formation requires the invention of new concepts, the
calculating of examples, the making of conjectures and the proving of
theorems. This book, representing four years of PhD work by Dr. Simon
Colton demonstrates how theory formation can be automated. Building on
over 20 years of research into constructing an automated mathematician
carried out in Professor Alan Bundy's mathematical reasoning group in
Edinburgh, Dr. Colton has implemented the HR system as a solution to the
problem of forming theories by computer. HR uses various pieces of
mathematical software, including automated theorem provers, model
generators and databases, to build a theory from the bare minimum of
information - the axioms of a domain. The main application of this work
has been mathematical discovery, and HR has had many successes. In
particular, it has invented 20 new types of number of sufficient
interest to be accepted into the Encyclopaedia of Integer Sequences, a
repository of over 60,000 sequences contributed by many (human)
mathematicians.