Formalization of Geometric Algebra in HOL Light
Formalization of Geometric Algebra in HOL Light
复制标题
HOL Light 中几何代数的形式化
DOI：
10.1007/s10817-018-9498-9
复制
发表时间：
2018-12
期刊：
影响因子：
--
通讯作者：
Li Yong Dong
中科院分区：
文献类型：
--
作者：
Li Li Ming;Shi Zhi Ping;Guan Yong;Zhang Qian Ying;Li Yong Dong
尽管几何代数（GA）理论在工程设计和分析中得到广泛应用，但对其形式化的研究却很少。本文提出了HOL Light中遗传算法相对完整的形式化。遗传算法理论的代数和几何部分相继被形式化。对于代数部分，基于具有三种类型度量的多向量的形式化定义，提出了一种统一的抽象乘积，以促进三种基本乘积的形式化。对于几何部分，首先给出了叶片和叶片及其关系的形式化公式。然后，在遗传算法的理论框架中形式化地表示了几种常用的特定空间。本文的新颖性在于两个方面：（a）定义了多向量类型（P，Q，R）geomalg，该定义为几何代数的形式化提供了最重要的基础；（b）开发了自动证明遗传算法运算性质的程序。本工作完善了HOL Light的功能，使得基于遗传算法的形式化分析和验证更加方便。
Although the theories of geometric algebra (GA) are widely applied in engineering design and analysis, the studies on their formalization have been scarcely conducted. This paper proposes a relatively complete formalization of GA in HOL Light. Both algebraic and geometric parts of the GA theories are formalized successively. For the algebraic part, a uniform abstract product is proposed to facilitate the formalization of the three basic products based on the formal definition of multivectors with three types of metrics. For the geometric part, the formal formulation is provided for the blades and versors and their relations at first. Then, several commonly used specific spaces are formally represented in the theoretical framework of GA. The novelty of the present paper lies in two aspects: (a) the multivector type,(P,Q,R)geomalg, is defined and the definition provides the most important foundation for the formalization of geometric algebra, and (b) a procedure is developed for automatically proving the properties of GA operations. The present work improves the function of HOL Light and makes the GA-based formal analysis and verification more convenient.
登录
查看更多内容
DOI：
--
发表时间：
2008-10
期刊：
arXiv: Mathematical Physics
影响因子：
--
作者：
Gerardo Aragon-Camarasa;G. Aragón-González;José L. Aragón;Andrade
通讯作者：
Gerardo Aragon-Camarasa;G. Aragón-González;José L. Aragón;Andrade
影响因子：
2.3
作者：
Hales, Thomas;Adams, Mark;Zumkeller, Roland
通讯作者：
Zumkeller, Roland
DOI：
10.1007/978-1-4612-0159-5_24
发表时间：
2001
期刊：
--
影响因子：
--
作者：
Stephen Mann;L. Dorst;T. Bouma
通讯作者：
Stephen Mann;L. Dorst;T. Bouma
DOI：
10.1119/1.14223
发表时间：
1984-06
期刊：
--
影响因子：
--
作者：
D. Hestenes;G. Sobczyk;J. S. Marsh
通讯作者：
D. Hestenes;G. Sobczyk;J. S. Marsh
DOI：
10.1016/j.vlsi.2008.09.010
发表时间：
2009-06
期刊：
Integr.
影响因子：
--
作者：
S. Franchini;A. Gentile;F. Sorbello;G. Vassallo;S. Vitabile
通讯作者：
S. Franchini;A. Gentile;F. Sorbello;G. Vassallo;S. Vitabile