Recenzie knihy Automated Theory Formation in Pure Mathematics - Colton, Simon

\nIntroduction.- 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.-... prečítať celé

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

Skryť popis