Managing automatically formed mathematical theories

Simon Colton, Pedro Torres, Paul Cairns, Volker Sorge

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Title of host publicationMathematical Knowledge Management - 5th International Conference, MKM 2006, Proceedings
Number of pages14
ISBN (Print)3540371044, 9783540371045
Publication statusPublished - 2006
Externally publishedYes
Event5th International Conference on Mathematical Knowledge Management, MKM 2006 - Wokingham, United Kingdom
Duration: 11 Aug 200612 Aug 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4108 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference5th International Conference on Mathematical Knowledge Management, MKM 2006
CountryUnited Kingdom

Cite this