Clifford代数与几何定理机器证明

Clifford Algebra and Automated Geometric Theorem Proving

Clifford代数是一种深深根植于几何学之中的代数系统。近年来 ,它在微分几何、理论物理、经典分析等方面取得了辉煌的成就 ,是现代理论数学和物理的一个核心工具 ,并在现代科技的各个领域 ,如机器人学、计算机视觉等方面有广泛的应用。本文主要介绍Clifford代数在数学机械化的核心内容—几何定理机器证明中的应用。作为一种非常优秀的描述和计算几何问题的代数语言 ,Clifford代数对于几何体 ,几何关系和几何变换有不依赖于坐标的、易于计算的多种表示 ,因而应用它进行几何自动推理 ,不仅使困难定理的证明往往变得极为简单 ,而且能够解决著名的数学公开问题。目前在国际上 ,几何自动推理已经成为Clif ford代数的一个重要应用领域。

Clifford algebra is algebraic system deeply rooted in geometry. In recent years, Clifford algebra has made spectacular achievements in differential geometry, theoretical physics and classical analysis. It is a central tool in modern mathematics and physics, and has wide ranged applications in robotics, computer vision, and other enginering fields. In this paper we introduce some applications of Clifford algebra in automated geometric theorem proving the kernel of mathematics mechanization. As a very elegant algebraic language for describing and computing geometric problems, Clifford algebra has a variety of coordinate free and computing favorable representations for geometric entites, relations and transformations. Therefore, applying Clifford algebra in automated geometric deduction can not only make the proof procedures extremely simple, but also solve some famous but open mathematical problems. Nowadays in the world, automated geometric deduction has become an important field for applying Clifford algebra.