rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    title: Automated Theory Formation in Pure Mathematics
  name:
    name part: Colton, Simon.
    role:
      role term: creator
  name:
    name part: SpringerLink (Online service)
  type of resource: text
  genre: Electronic books.
  origin info:
    place:
      place term: enk
    date issued: 2002
    issuance: monographic
  language:
    language term: eng
  physical description:
    form: remote
    extent: 1 online resource (XVI, 380 pages)
  abstract: 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.
  table of contents: Introduction -- Literature Survey -- Mathematical Theories -- Design Considerations -- Background Knowledge -- Inventing Concepts -- Making Conjectures -- Settling Conjectures -- Assessing Concepts -- Assessing Conjectures -- An Evaluation of HR's Theories -- The Application of HR to Discovery Tasks -- Related Work -- Further Work -- Conclusions -- Appendix A: User Manual for HR 1.11 -- Appendix B: Example Sessions -- Appendix C: Number Theory Results.
  note: by Simon Colton.
  note: Electronic resource.
  subject:
    topic: Computer science
  subject:
    topic: Artificial intelligence
  subject:
    topic: Artificial intelligence
  subject:
    topic: Computer science
  classification: Q334-342
  classification: 006.3
  related item:
    title info:
      title: Distinguished dissertations
  identifier: 9781447101475 (electronic bk.)
  identifier: 1447101472 (electronic bk.)
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: I9W
    record creation date: 121227
    record change date: 20260420215008.4
    record identifier: in00003545212
    language of cataloging:
      language term: eng