The Resource Automated Theory Formation in Pure Mathematics, by Simon Colton, (electronic resource)

Automated Theory Formation in Pure Mathematics, by Simon Colton, (electronic resource)

Label
Automated Theory Formation in Pure Mathematics
Title
Automated Theory Formation in Pure Mathematics
Statement of responsibility
by Simon Colton
Creator
Author
Author
Subject
Language
  • eng
  • eng
Summary
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
Member of
http://library.link/vocab/creatorName
Colton, Simon
Dewey number
510
http://bibfra.me/vocab/relation/httpidlocgovvocabularyrelatorsaut
_GAWoukBRlM
Image bit depth
0
Language note
English
LC call number
QA1-939
Literary form
non fiction
Nature of contents
dictionaries
Series statement
Distinguished Dissertations
http://library.link/vocab/subjectName
  • Mathematics
  • Artificial intelligence
  • Computer science
  • Mathematics, general
  • Artificial Intelligence
  • Math Applications in Computer Science
Label
Automated Theory Formation in Pure Mathematics, by Simon Colton, (electronic resource)
Instantiates
Publication
Note
Bibliographic Level Mode of Issuance: Monograph
Antecedent source
mixed
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
cr
Color
not applicable
Content category
text
Content type code
txt
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
Dimensions
unknown
Edition
1st ed. 2002.
Extent
1 online resource (XVI, 380 p.)
File format
multiple file formats
Form of item
online
Isbn
9781447101475
Level of compression
uncompressed
Media category
computer
Media type code
c
Other control number
10.1007/978-1-4471-0147-5
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
System control number
  • (CKB)3400000000088004
  • (SSID)ssj0000933628
  • (PQKBManifestationID)11513287
  • (PQKBTitleCode)TC0000933628
  • (PQKBWorkID)10891135
  • (PQKB)11570178
  • (DE-He213)978-1-4471-0147-5
  • (MiAaPQ)EBC3073690
  • (EXLCZ)993400000000088004
Label
Automated Theory Formation in Pure Mathematics, by Simon Colton, (electronic resource)
Publication
Note
Bibliographic Level Mode of Issuance: Monograph
Antecedent source
mixed
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
cr
Color
not applicable
Content category
text
Content type code
txt
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
Dimensions
unknown
Edition
1st ed. 2002.
Extent
1 online resource (XVI, 380 p.)
File format
multiple file formats
Form of item
online
Isbn
9781447101475
Level of compression
uncompressed
Media category
computer
Media type code
c
Other control number
10.1007/978-1-4471-0147-5
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
System control number
  • (CKB)3400000000088004
  • (SSID)ssj0000933628
  • (PQKBManifestationID)11513287
  • (PQKBTitleCode)TC0000933628
  • (PQKBWorkID)10891135
  • (PQKB)11570178
  • (DE-He213)978-1-4471-0147-5
  • (MiAaPQ)EBC3073690
  • (EXLCZ)993400000000088004

Library Locations

  • Architecture LibraryBorrow it
    Gould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US
    35.205706 -97.445050
  • Bizzell Memorial LibraryBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Boorstin CollectionBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Chinese Literature Translation ArchiveBorrow it
    401 W. Brooks St., RM 414, Norman, OK, 73019, US
    35.207487 -97.447906
  • Engineering LibraryBorrow it
    Felgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US
    35.205706 -97.445050
  • Fine Arts LibraryBorrow it
    Catlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US
    35.210371 -97.448244
  • Harry W. Bass Business History CollectionBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • History of Science CollectionsBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • John and Mary Nichols Rare Books and Special CollectionsBorrow it
    401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • Library Service CenterBorrow it
    2601 Technology Place, Norman, OK, 73019, US
    35.185561 -97.398361
  • Price College Digital LibraryBorrow it
    Adams Hall 102 307 West Brooks St., Norman, OK, 73019, US
    35.210371 -97.448244
  • Western History CollectionsBorrow it
    Monnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US
    35.209584 -97.445414
Processing Feedback ...