TY - GEN

T1 - Managing automatically formed mathematical theories

AU - Colton, Simon

AU - Torres, Pedro

AU - Cairns, Paul

AU - Sorge, Volker

PY - 2006

Y1 - 2006

N2 - The HR system forms scientific theories, and has found particularly successful application in domains of pure mathematics, Starting with only the axioms of an algebraic system, HR can generate dozens of example algebras, hundreds of concepts and thousands of conjectures, many of which have first order proofs. Given the overwhelming amount of knowledge produced, we have provided HR with sophisticated tools for handling this data. We present here the first full description of these management tools. Moreover, we describe how careful analysis of the theories produced by HR - which is enabled by the management tools - has led us to make interesting discoveries in algebraic domains. We demonstrate this with some illustrative results from HR's theories about an algebra of one axiom. The results fueled further developments, and led us to discover and prove a fundamental theorem about this domain.

AB - The HR system forms scientific theories, and has found particularly successful application in domains of pure mathematics, Starting with only the axioms of an algebraic system, HR can generate dozens of example algebras, hundreds of concepts and thousands of conjectures, many of which have first order proofs. Given the overwhelming amount of knowledge produced, we have provided HR with sophisticated tools for handling this data. We present here the first full description of these management tools. Moreover, we describe how careful analysis of the theories produced by HR - which is enabled by the management tools - has led us to make interesting discoveries in algebraic domains. We demonstrate this with some illustrative results from HR's theories about an algebra of one axiom. The results fueled further developments, and led us to discover and prove a fundamental theorem about this domain.

UR - http://www.scopus.com/inward/record.url?scp=33749549378&partnerID=8YFLogxK

M3 - Conference Paper

AN - SCOPUS:33749549378

SN - 3540371044

SN - 9783540371045

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 237

EP - 250

BT - Mathematical Knowledge Management - 5th International Conference, MKM 2006, Proceedings

PB - Springer

T2 - 5th International Conference on Mathematical Knowledge Management, MKM 2006

Y2 - 11 August 2006 through 12 August 2006

ER -