Combining AI systems for classification in non-associative algebra

Volker Sorge, Andreas Meier, Roy McCasland, Simon Colton

Research output: Contribution to conferencePaperpeer-review


The automatic construction of mathematical theorems is a challenging task for Artificial Intelligence systems, which has pushed many research boundaries in different branches of AI. We describe how the construction of classification theorems in algebraic domains of mathematics has driven research not only on the individual mathematical reasoning techniques, but also the integration of these techniques. We have developed a bootstrapping algorithm for the automatic generation of such theorems which relies on the power of model generation, first order theorem proving, computer algebra, machine learning and satisfiability solving. In particular, the construction of algebraic invariants demands an intricate interplay of these techniques. We demonstrate the effectiveness of this approach by generating novel theorems which have so far been beyond the reach of automated reasoning systems.

Original languageEnglish
Number of pages14
Publication statusPublished - 1 Jan 2006
Externally publishedYes
EventSymposium on the Integration of Symbolic Computation and Mechanized Reasoning 2006 - Genova, Italy
Duration: 7 Jul 20069 Jul 2006
Conference number: 13th


ConferenceSymposium on the Integration of Symbolic Computation and Mechanized Reasoning 2006
Abbreviated titleCalculemus 2006


  • Automated discovery
  • Finite algebra

Cite this