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 -