Automatic Generation of Classification Theorems for Finite Algebras
Automatic Generation of Classification Theorems for Finite Algebras
复制标题
自动生成有限代数分类定理
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
R. McCasland
中科院分区：
文献类型：
--
作者：
S. Colton;A. Meier;V. Sorge;R. McCasland
有限代数结构的分类一直是纯数学研究背后的主要动机。自动化技术有助于这一过程，但这在很大程度上是在定量水平上。相比之下，我们提出了一个定性的方法，产生验证定理，分类代数的特定类型和大小到同构类。我们描述了一个半自动和全自动的自举方法来建立和验证分类定理。在后一种情况下，我们已经实现了一个程序，该程序采用代数的公理，并产生一个嵌入了一个经过充分验证的分类定理的决策树。这是通过集成（和改进）一些自动推理技术来实现的：我们使用Mace模型生成器，HR和C4.5机器学习系统，Spass定理证明器和差距计算机代数系统来降低Spass问题的复杂性。我们证明了这种方法的力量，通过分类循环，组，幺半群和各种大小的拟群。
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.