Automatic Concept Formation in Pure Mathematics

Simon Colton; Alan Bundy; Toby Walsh

Automatic Concept Formation in Pure Mathematics

Simon Colton, Alan Bundy, Toby Walsh

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras.

Original language	English
Title of host publication	Proceedings of the 16th international joint conference on Artificial Intelligence - IJCAI '99
Publisher	MORGAN KAUFMANN PUB INC
Pages	786-791
ISBN (Print)	1-55860-613-0
Publication status	Published - 1999

Access to Document

Full textAccepted author manuscript, 199 KB

http://hdl.handle.net/1842/4570

Cite this

@inproceedings{14c28f81cf9549dbb57f915e98ddd5bb,

title = "Automatic Concept Formation in Pure Mathematics",

abstract = "The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras.",

author = "Simon Colton and Alan Bundy and Toby Walsh",

year = "1999",

language = "English",

isbn = "1-55860-613-0",

pages = "786--791",

booktitle = "Proceedings of the 16th international joint conference on Artificial Intelligence - IJCAI '99",

publisher = "MORGAN KAUFMANN PUB INC",

}

TY - GEN

T1 - Automatic Concept Formation in Pure Mathematics

AU - Colton, Simon

AU - Bundy, Alan

AU - Walsh, Toby

PY - 1999

Y1 - 1999

N2 - The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras.

AB - The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of interesting new mathematics and enables it to build theories from just the axioms of finite algebras.

M3 - Conference contribution

SN - 1-55860-613-0

SP - 786

EP - 791

BT - Proceedings of the 16th international joint conference on Artificial Intelligence - IJCAI '99

PB - MORGAN KAUFMANN PUB INC

ER -

Automatic Concept Formation in Pure Mathematics

Abstract / Description of output

Access to Document

Fingerprint

Cite this