论文标题
有限群体理论的形式化
A Formalization of Finite Group Theory
论文作者
论文摘要
基于“封装”或“ defn-sk”的ACL2和NQTHM中的组理论的先前表述，由于他们未能通过诱导群体的顺序提供证明途径的限制，这是Lagrange定理以外的该领域中最有趣的结果所必需的（声称由一个子组的群体分解）。我们描述了有限群体理论的替代方法，该方法基于组作为操作表的明确表示，可以补救这种缺陷。我们定义一个用于生成组的参数化家族的“ Deffroup”宏，我们将其应用于整数模拟的添加剂和乘法组，对称组，任意商组和环状亚组。除了Lagrange定理的证明外，我们还提出了Cauchy定理的Abelian案例的感应证明：如果G组的顺序被Prime P分解，则G具有顺序p的元素。
Previous formulations of group theory in ACL2 and Nqthm, based on either "encapsulate" or "defn-sk", have been limited by their failure to provide a path to proof by induction on the order of a group, which is required for most interesting results in this domain beyond Lagrange's Theorem (asserting the divisibility of the order of a group by that of a subgroup). We describe an alternative approach to finite group theory that remedies this deficiency, based on an explicit representation of a group as an operation table. We define a "defgroup" macro for generating parametrized families of groups, which we apply to the additive and multiplicative groups of integers modulo n, the symmetric groups, arbitrary quotient groups, and cyclic subgroups. In addition to a proof of Lagrange's Theorem, we present an inductive proof of the abelian case of a theorem of Cauchy: If the order of a group G is divisible by a prime p, then G has an element of order p.
