Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Automatic Generation of Classification Theorems for Finite Algebras
Authors: Simon Colton ; Andreas Meier ; Volker Sorge ; Roy McCasland
Date:Jul 2004
Publication Title:Proceedings of IJCAR 2004 (LNCS 3097)
Publisher:Springer Verlag
Publication Type:Conference Paper Publication Status:Published
Volume No:3097 Page Nos:400-414
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 power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.
Links To Paper
1st Link
Bibtex format
author = { Simon Colton and Andreas Meier and Volker Sorge and Roy McCasland },
title = {Automatic Generation of Classification Theorems for Finite Algebras},
book title = {Proceedings of IJCAR 2004 (LNCS 3097)},
publisher = {Springer Verlag},
year = 2004,
month = {Jul},
volume = {3097},
pages = {400-414},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh