秩为2的旋转自由群
计算机科学中的逻辑
2022-05-25 v1
摘要
Banach-Tarski 定理证明中的关键步骤之一是引入一个旋转自由群。首先，生成一个由简约词组成的自由群，其中集合中的每个元素都表示为一个 ACL2 列表。然后我们证明简约词集合与一组三维旋转之间存在一一对应关系。在本文中，我们提出了一种生成该简约词集合的方法，并证明了该集合的群性质。接着，我们展示了一种利用简约词集合生成三维矩阵集合的方法。最后我们给出了三维旋转的形式化描述，并证明三维矩阵集合中的每个元素都是一个旋转。
引用
@article{arxiv.2205.11699,
title = {A Free Group of Rotations of Rank 2},
author = {Jagadish Bapanapally and Ruben Gamboa},
journal= {arXiv preprint arXiv:2205.11699},
year = {2022}
}
备注
In Proceedings ACL2 2022, arXiv:2205.11103