Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
Automated Theory Formation in Pure Mathematics

Automated Theory Formation in Pure Mathematics

Aus der Reihe
Gebundenes Buch

Gebundenes Buch

Fr. 161.00 Taschenbuch

Taschenbuch

Fr. 138.00 eBook

eBook

Fr. 125.90

Automated Theory Formation in Pure Mathematics

Ebenfalls verfügbar als:

Gebundenes Buch

Gebundenes Buch

ab Fr. 161.00
Taschenbuch

Taschenbuch

ab Fr. 138.00
eBook

eBook

ab Fr. 125.90

Fr. 138.00

inkl. MwSt, Versandkostenfrei

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

27.09.2012

Verlag

Springer London

Seitenzahl

380

Maße (L/B/H)

23.5/15.5/2.2 cm

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

27.09.2012

Verlag

Springer London

Seitenzahl

380

Maße (L/B/H)

23.5/15.5/2.2 cm

Gewicht

604 g

Auflage

Softcover reprint of the original 1st ed. 2002

Sprache

Englisch

ISBN

978-1-4471-1113-9

Herstelleradresse

Springer-Verlag London Ltd.
Old Portsmouth Road
GU3 1LT Guildford, Surrey
GB
Email: sdc-bookservice@springer.com
Telephone: +49 6221 3454301
Fax: +49 6221 3454229

Weitere Bände von Distinguished Dissertations

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Erste Bewertung verfassen

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen filtern
  • Automated Theory Formation in Pure Mathematics
  • 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 Valdés-Pérez’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.