Automatic Generation of Classification Theorems for Finite Algebras

Abstract. Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a quantitative level. In contrast, we present a qualitative approach which produces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying classification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree embedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer algebra system to reduce the complexity of the problems given to Spass. We demonstrate the...

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Simon Colton, Andreas Meier, Volker Sorge, Roy L. McCasland
• Keywords: Automated Reasoning, CADE 2004, Finite Algebraic Structures, Mace Model Generator, Machine Learning Systems