## Abstract

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 language | English |
---|---|

Pages | 100-113 |

Number of pages | 14 |

Publication status | Published - 1 Jan 2006 |

Externally published | Yes |

Event | Symposium on the Integration of Symbolic Computation and Mechanized Reasoning 2006 - Genova, Italy Duration: 7 Jul 2006 → 9 Jul 2006 Conference number: 13th |

### Conference

Conference | Symposium on the Integration of Symbolic Computation and Mechanized Reasoning 2006 |
---|---|

Abbreviated title | Calculemus 2006 |

Country | Italy |

City | Genova |

Period | 7/07/06 → 9/07/06 |

## Keywords

- Automated discovery
- Finite algebra