عنوان

Automated Theory Formation in Pure Mathematics

شابک

1447101472

شابک

1447111133

شابک

9781447101475

شابک

9781447111139

شماره

b548767

عنوان اصلي

Automated Theory Formation in Pure Mathematics

نام عام مواد

[Book]

نام نخستين پديدآور

by Simon Colton.

محل نشرو پخش و غیره

London

نام ناشر، پخش کننده و غيره

Springer London

تاریخ نشرو بخش و غیره

2002

نام خاص و کميت اثر

.

عنوان فروست

Distinguished Dissertations

متن يادداشت

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.2.1 The AM Program.- 2.2.2 The GT Program.- 2.2.3 The IL Program.- 2.2.4 The Bagai et al. Program.- 2.3 The BACON Programs.- 2.4 Concept Invention.- 2.4.1 The Representation of Mathematical Concepts.- 2.4.2 Inductive Logic Programming.- 2.5 Conjecture Making Programs.- 2.5.1 The Graffiti Program.- 2.5.2 The AutoGraphiX Program.- 2.5.3 The PSLQ Algorithm.- 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.1.1 Group Theory.- 3.1.2 Graph Theory.- 3.1.3 Number Theory.- 3.1.4 Isomorphism.- 3.2 Mathematical Domains.- 3.2.1 Reasons Behind Theory Formation.- 3.2.2 Finite and Infinite Domains.- 3.3 The Content of Theories.- 3.3.1 Concepts.- 3.3.2 Conjectures, Theorems and Proofs.- 3.3.3 Other Aspects of Theories.- 3.4 Summary.- 4. Design Considerations.- 4.1 Aspects of Theory Formation.- 4.1.1 Aspects Which are Modelled.- 4.1.2 Some Aspects Which are not Modelled.- 4.2 Concept and Conjecture Making Decisions.- 4.2.1 The Use of Examples.- 4.2.2 Making Conjectures.- 4.3 The Domains HR Works in.- 4.4 Representation Issues.- 4.4.1 Examples of Concepts.- 4.4.2 Definitions of Concepts.- 4.4.3 Representation of Conjectures, Proofs and Counterexamples.- 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.3.1 Initial Concepts in Graph Theory.- 5.3.2 Initial Concepts in Number Theory.- 5.3.3 Initial Concepts in Finite Algebraic Systems.- 5.4 Generating Initial Concepts from Axioms.- 5.5 Summary.- 6. Inventing Concepts.- 6.1 An Overview of the Production Rules.- 6.1.1 Some Common Construction Techniques.- 6.2 The Exists Production Rule.- 6.2.1 Data Table Construction and Parameterisations.- 6.2.2 Generation of Definitions.- 6.3 The Match Production Rule.- 6.3.1 Data Table Construction and Parameterisations.- 6.3.2 Generation of Definitions.- 6.4 The Negate Production Rule.- 6.4.1 Data Table Construction and Parameterisations.- 6.4.2 Generation of Definitions.- 6.5 The Size Production Rule.- 6.5.1 Data Table Construction and Parameterisation.- 6.5.2 Generation of Definitions.- 6.6 The Split Production Rule.- 6.6.1 Data Table Construction and Parameterisations.- 6.6.2 Generation of Definitions.- 6.7 The Compose Production Rule.- 6.7.1 Data Table Construction and Parameterisations.- 6.7.2 Generation of Definitions.- 6.7.3 Generalisation of Previous Production Rules.- 6.8 The Forall Production Rule.- 6.8.1 Data Table Construction and Parameterisations.- 6.8.2 Generation of Definitions.- 6.9 Efficiency and Soundness Considerations.- 6.9.1 Forbidden Paths.- 6.9.2 Generated and Stored Properties.- 6.9.3 Proving Consistency Between Data Tables and Definitions.- 6.10 Example Constructions.- 6.11 Summary.- 7. Making Conjectures.- 7.1 Equivalence Conjectures.- 7.1.1 Making Equivalence Conjectures Automatically.- 7.1.2 Implementation Details.- 7.2 Implication Conjectures.- 7.2.1 Making Implication Conjectures Automatically.- 7.2.2 Implementation Details.- 7.3 Non-existence Conjectures.- 7.3.1 Making Non-existence Conjectures Automatically.- 7.4 Applicability Conjectures.- 7.4.1 Making Applicability Conjectures Automatically.- 7.4.2 Implementation Details.- 7.5 Conjecture Making Using the Encyclopedia of Integer Sequences.- 7.5.1 Presenting Concepts as Integer Sequences.- 7.5.2 Conjecture Types.- 7.5.3 Pruning Methods.- 7.5.4 An Example Conjecture.- 7.6 Issues in Automated Conjecture Making.- 7.6.1 Choice of Conjecture Making Techniques.- 7.6.2 When to Check for Conjectures.- 7.6.3 The Use of Data and Pruning Methods.- 7.6.4 Other Conjecture Formats.- 7.7 Summary.- 8. Settling Conjectures.- 8.1 Reasons for Settling Conjectures.- 8.2 Proving Conjectures.- 8.2.1 Using Otter to Prove Conjectures.- 8.2.2 Sub-conjectures and Prime Implicates.- 8.2.3 Using HR to Prove Implication Conjectures.- 8.2.4 Details of HR's Theorem Proving.- 8.2.5 Advantages of Using HR to Prove Theorems.- 8.3 Disproving Conjectures.- 8.3.1 Using MACE to Find Counterexamples.- 8.3.2 Using HR to Find Counterexamples.- 8.3.3 Finding Counterexamples in Non-algebraic Domains.- 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.2.1 What Makes a Concept Interesting?.- 9.2.2 What Makes a Concept Uninteresting?.- 9.2.3 Interestingness Gained from Theory Formation.- 9.3 Intrinsic and Relational Measures of Concepts.- 9.3.1 Comprehensibility.- 9.3.2 Parsimony.- 9.3.3 Applicability.- 9.3.4 Novelty.- 9.4 Utilitarian Properties of Concepts.- 9.4.1 Productivity.- 9.4.2 Classification Tasks.- 9.5 Conjectures about Concepts.- 9.6 Details of the Heuristic Searches.- 9.6.1 When and How to Measure Concepts.- 9.6.2 Sorting the Production Rules.- 9.6.3 Restricting the Search.- 9.6.4 Choosing Weights.- 9.7 Worked Example.- 9.8 Other Possibilities.- 9.9 Summary.- 10. Assessing Conjectures.- 10.1 Generic Measures for Conjectures.- 10.1.1 Type of Conjecture.- 10.1.2 Surprisingness.- 10.1.3 Other Generic Measures.- 10.2 Additional Measures for Theorems.- 10.2.1 Difficulty of Proof.- 10.2.2 Generality of Theorems.- 10.3 Additional Measures for Non-theorems.- 10.4 Setting Weights for Conjecture Measures.- 10.5 Assessing Concepts Using Conjectures.- 10.5.1 Independence of Measures for Conjectures.- 10.5.2 Identifying Concepts Discussed in Conjectures.- 10.5.3 Measures for Concepts.- 10.6 Worked Example.- 10.7 Summary.- 11. An Evaluation of HR's Theories.- 11.1 Analysis of Two Theories.- 11.1.1 A Theory of Numbers.- 11.1.2 A Theory of Groups.- 11.2 Desirable Qualities of Theories - Concepts.- 11.2.1 Average Applicability of Concepts.- 11.2.2 Average Comprehensibility of Concepts.- 11.2.3 Number of Categorisations.- 11.2.4 Number of Concepts.- 11.3 Desirable Qualities of Theories - Conjectures.- 11.3.1 Difficulty and Surprisingness of Conjectures.- 11.3.2 Proportion of Theorems and Open Conjectures.- 11.4 Using the Heuristic Search.- 11.4.1 Robustness of the Heuristic Measures.- 11.4.2 Differences Between Domains.- 11.4.3 Pruning Using the Heuristic Measures.- 11.5 Classically Interesting Results.- 11.5.1 Graph Theory.- 11.5.2 Group Theory.- 11.5.3 Number Theory.- 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.3.1 Additions to the Encyclopedia.- 12.3.2 Refactorable Numbers.- 12.3.3 Sequence A046951.- 12.4 Discovery Task Failures.- 12.5 Valdes-Perez's Machine Discovery Criteria.- 12.5.1 Novelty.- 12.5.2 Interestingness.- 12.5.3 Plausibility.- 12.5.4 Intelligibility.- 12.6 Conclusions.- 13.

متن يادداشت

Related Work.- 13.1 A Comparison of HR and the AM Program.- 13.1.1 How AM Formed Theories.- 13.1.2 Misconceptions about AM.- 13.1.3 Programs Based on AM.- 13.1.4 A Qualitative Comparison of AM and HR.- 13.1.5 A Quantitative Comparison of AM and HR.- 13.1.6 Summary: The AM Program.- 13.2 A Comparison of HR and the GT Program.- 13.2.1 How GT Formed Theories.- 13.2.2 The SCOT Program.- 13.2.3 A Qualitative Comparison of GT and HR.- 13.2.4 A Quantitative Comparison of GT and HR.- 13.3 A Comparison of HR and the IL Program.- 13.3.1 How IL Worked.- 13.3.2 A Qualitative Comparison of IL and HR.- 13.4 A Comparison of HR and Bagai et al's Program.- 13.4.1 How Bagai et al's Program Worked.- 13.4.2 A Qualitative Comparison of HR and Bagai et al's Program.- 13.5 A Comparison of HR and the Graffiti Program.- 13.5.1 How Graffiti Works.- 13.5.2 A Qualitative Comparison of Graffiti and HR.- 13.6 A Comparison of HR and the Progol Program.- 13.7 Summary.- 14. Further Work.- 14.1 Additional Theory Formation Abilities.- 14.1.1 Additional Production Rules.- 14.1.2 Improved Presentational Aspects.- 14.1.3 Further Possibilities for Making and Settling Conjectures.- 14.2 The Application of Theory Formation.- 14.2.1 Automated Conjecture Making in Mathematics.- 14.2.2 Constraint Satisfaction Problems.- 14.2.3 Machine Learning.- 14.2.4 Automated Theorem Proving.- 14.2.5 Application to Other Scientific Domains.- 14.3 Theoretical Explorations.- 14.3.1 Meta-theory Formation.- 14.3.2 Cross Domain Theory Formation.- 14.3.3 Agent Based Cooperative Theory Formation.- 14.4 Summary.- 15. Conclusions.- 15.1 Have We Achieved Our Aims?.- 15.2 Contributions.- 15.2.1 Functionality.- 15.2.2 Simplicity of Architecture.- 15.2.3 Cycle of Mathematical Activity.- 15.2.4 Generality of Methods.- 15.2.5 Mathematical Discovery.- 15.2.6 Evaluation Techniques.- 15.3 Automated Theory Formation in Pure Maths.- Appendix A. User Manual for HR1.11.- Appendix B. Example Sessions.- Appendix C. Number Theory Results.

شماره رده

نشانه اثر

مستند نام اشخاص تاييد نشده

by Simon Colton.

مستند نام اشخاص تاييد نشده

Simon Colton

نام الکترونيکي

نوع ماده

[Book]

تكميل شده

Y