Colton, Simon; Meier, Andreas; Sorge, Volker; McCasland, Roy Automatic generation of classification theorems for finite algebras. (English) Zbl 1126.68562 Basin, David (ed.) et al., Automated reasoning. Second international joint conference, IJCAR 2004, Cork, Ireland, July 4–8, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22345-2/pbk). Lecture Notes in Computer Science 3097. Lecture Notes in Artificial Intelligence, 400-414 (2004). Summary: 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.For the entire collection see [Zbl 1088.68001]. Cited in 3 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 08-04 Software, source code, etc. for problems pertaining to general algebraic systems 20-04 Software, source code, etc. for problems pertaining to group theory Software:C4.5; Mace4; HR; SPASS; GAP PDFBibTeX XMLCite \textit{S. Colton} et al., Lect. Notes Comput. Sci. 3097, 400--414 (2004; Zbl 1126.68562) Full Text: DOI