Automated Theory Formation in Pure Mathematics / Edition 1

by Simon Colton

Overview

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.

Product Details

ISBN-13:	9781852336097
Publisher:	Springer London
Publication date:	09/17/2002
Series:	Distinguished Dissertations
Edition description:	2002
Pages:	380
Product dimensions:	6.10(w) x 9.25(h) x 0.24(d)

Table of Contents

1. Introduction.- 1.1 Motivation.- 1.2 Aims of the Project.- 1.3 Contributions.- 1.4 Organisation of the Book.- 1.5 Summary.- 2. Literature Survey.- 2.1 Some Philosophical Issues.- 2.2 Mathematical Theory Formation Programs.- 2.3 The BACON Programs.- 2.4 Concept Invention.- 2.5 Conjecture Making Programs.- 2.6 The Otter and MACE Programs.- 2.7 The Encyclopedia of Integer Sequences.- 2.8 Summary.- 3. Mathematical Theories.- 3.1 Group Theory, Graph Theory and Number Theory.- 3.2 Mathematical Domains.- 3.3 The Content of Theories.- 3.4 Summary.- 4. Design Considerations.- 4.1 Aspects of Theory Formation.- 4.2 Concept and Conjecture Making Decisions.- 4.3 The Domains HR Works in.- 4.4 Representation Issues.- 4.5 The HR Program in Outline.- 4.6 Summary.- 5. Background Knowledge.- 5.1 Objects of Interest (Entities).- 5.2 Required Information about Concepts.- 5.3 Initial Concepts from the User.- 5.4 Generating Initial Concepts from Axioms.- 5.5 Summary.- 6. Inventing Concepts.- 6.1 An Overview of the Production Rules.- 6.2 The Exists Production Rule.- 6.3 The Match Production Rule.- 6.4 The Negate Production Rule.- 6.5 The Size Production Rule.- 6.6 The Split Production Rule.- 6.7 The Compose Production Rule.- 6.8 The Forall Production Rule.- 6.9 Efficiency and Soundness Considerations.- 6.10 Example Constructions.- 6.11 Summary.- 7. Making Conjectures.- 7.1 Equivalence Conjectures.- 7.2 Implication Conjectures.- 7.3 Non-existence Conjectures.- 7.4 Applicability Conjectures.- 7.5 Conjecture Making Using the Encyclopedia of Integer Sequences.- 7.6 Issues in Automated Conjecture Making.- 7.7 Summary.- 8. Settling Conjectures.- 8.1 Reasons for Settling Conjectures.- 8.2 Proving Conjectures.- 8.3 Disproving Conjectures.- 8.4 Returning to Open Conjectures.- 8.5 Summary.- 9. Assessing Concepts.- 9.1 The Agenda Mechanism.- 9.2 The Interestingness of Mathematical Concepts.- 9.3 Intrinsic and Relational Measures of Concepts.- 9.4 Utilitarian Properties of Concepts.- 9.5 Conjectures about Concepts.- 9.6 Details of the Heuristic Searches.- 9.7 Worked Example.- 9.8 Other Possibilities.- 9.9 Summary.- 10. Assessing Conjectures.- 10.1 Generic Measures for Conjectures.- 10.2 Additional Measures for Theorems.- 10.3 Additional Measures for Non-theorems.- 10.4 Setting Weights for Conjecture Measures.- 10.5 Assessing Concepts Using Conjectures.- 10.6 Worked Example.- 10.7 Summary.- 11. An Evaluation of HR’s Theories.- 11.1 Analysis of Two Theories.- 11.2 Desirable Qualities of Theories — Concepts.- 11.3 Desirable Qualities of Theories — Conjectures.- 11.4 Using the Heuristic Search.- 11.5 Classically Interesting Results.- 11.6 Conclusions.- 12. The Application of HR to Discovery Tasks.- 12.1 A Classification Problem.- 12.2 Exploration of an Algebraic System.- 12.3 Invention of Integer Sequences.- 12.4 Discovery Task Failures.- 12.5 Valdés-Pérez’s Machine Discovery Criteria.- 12.6 Conclusions.- 13. Related Work.- 13.1 A Comparison of HR and the AM Program.- 13.2 A Comparison of HR and the GT Program.- 13.3 A Comparison of HR and the IL Program.- 13.4 A Comparison of HR and Bagai et al’s Program.- 13.5 A Comparison of HR and the Graffiti Program.- 13.6 A Comparison of HR and the Progol Program.- 13.7 Summary.- 14. Further Work.- 14.1 Additional Theory Formation Abilities.- 14.2 The Application of Theory Formation.- 14.3 Theoretical Explorations.- 14.4 Summary.- 15. Conclusions.- 15.1 Have We Achieved Our Aims?.- 15.2 Contributions.- 15.3 Automated Theory Formation in Pure Maths.- Appendix A. User Manual for HR1.11.- Appendix B. Example Sessions.-Appendix C. Number Theory Results.