Automated theory formation in pure mathematics

Simon Colton

396 pages, parution le 27/09/2002

Ajouter à une liste

Indisponible

Résumé

In recent years, Artificial Intelligence researchers have largely focused their efforts on solving specific problems, with less emphasis on 'the big picture1- automating large scale tasks which require human-level intelligence to undertake. Automated theory formation requires the invention of new concepts, the calculating of examples, the making of conjectures and the proving of theorems. Representing four years of PhD work by Dr. Simon Colton, this book 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.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

Caractéristiques techniques

	PAPIER
Éditeur(s)	Springer
Auteur(s)	Simon Colton
Parution	27/09/2002
Nb. de pages	396
Format	16 x 24
Couverture	Relié
Poids	733g
Intérieur	Noir et Blanc
EAN13	9781852336097
ISBN13	978-1-85233-609-7