- 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 power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0371,
- 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 = {http://springerlink.metapress.com/link.asp?id=vuttuqx43c6we002},
- }
|
