Formalization of geometric algebra theories in higher-order logic

被引：0
|
作者：
Ma S. [1 ,2 ]
Shi Z.-P. [1 ,3 ]
Li L.-M. [1 ]
Guan Y. [1 ,3 ]
Zhang J. [4 ]
Song X. [5 ]
机构：
[1] Light Industrial Robot and Safety Verification of Key Laboratory of Beijing (Capital Normal University), Beijing
[2] Sophisticated Imaging Technology Innovation Center of Capital Normal University, Beijing
[3] Beijing Mathematics and Information Science 2011 Collaborative Innovation Center, Beijing
[4] College of Information Science & Technology, Beijing University of Chemical Technology, Beijing
[5] Electrical and Computer Engineering, Portland State University, Portland
来源：
Shi, Zhi-Ping (zhizp@cnu.edu.cn) | 1600年 / Chinese Academy of Sciences卷 / 27期
基金：
中国国家自然科学基金;
关键词：
Formal verification; Geometric algebra; Geometric product; HOL-Light; Theorem proving;
D O I：
10.13328/j.cnki.jos.004977
中图分类号：
学科分类号：
摘要：
Geometric algebra (GA) is an algebraic language used to describe and calculate geometric problems. Due to its unified expression and coordinate-free geometric calculation, GA has now become an important theoretical foundation and calculation tool in mathematical analysis, theoretical physics, geometry and many other fields. While being widely used in the areas of modern science and technology, GA based analysis is traditionally performed using computer based numerical techniques or symbolic methods. However, both of these techniques cannot guarantee the analysis accuracy for safety-critical applications. The higher order-logic theorem proving is one of the rigorous formal methods. This paper establishes a formal model of GA in the higher-order logic proof tool HOL Light. The proof of the correctness is provided for some definitions and properties including blade, multivector, outer product, inner product, geometric product, inverse, dual, operation rules of basis vector and transform operator. In order to illustrate the practical effectiveness and utilization of this formalization, a conformal geometric model is established to provide a simple and effective way on rigid body motion verification. © Copyright 2016, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
下载
收藏
页码：497 / 516
页数：19
相关论文
共 28 条
  • [1] Dorst L., Lasenby C.D.J., Applications of Geometric Algebra in Computer Science and Engineering, pp. 1-8, (2002)
  • [2] Bayro Corrochano E., Geometric Computing: for Wavelet Transforms, Robot Vision, Learning, Control and Action, pp. 3-49, (2010)
  • [3] Chappell J.M., Drake S.P., Seidel C.L., Gunn L.J., Iqbal A., Allison A., Abbott D., Geometric algebra for electrical and electronic engineers, Proc. of the IEEE, 102, 9, pp. 1340-1363, (2014)
  • [4] Choi H.I., Lee D.S., Moon H.P., Clifford algebra, spin representation, and rational parameterization of curves and surfaces, Advances in Computational Mathematics, 17, 1-2, pp. 5-48, (2002)
  • [5] Hildenbrand D., Geometric computing in computer graphics using conformal geometric algebra, Computers & Graphics, 29, 5, pp. 795-803, (2005)
  • [6] Hildenbrand D., Pitt J., Koch A., Gaalop-High Performance Parallel Computing Based on Conformal Geometric Algebra, pp. 477-494, (2010)
  • [7] Siddique U., Hasan O., On the Formalization of Gamma Function in HOL, Journal of Automated Reasoning, 53, 4, pp. 407-429, (2014)
  • [8] Klein G., Elphinstone K., Heiser G., Andronick J., Formal verification of an OS kernel, Proc. of the 22nd ACM Symp. on Operating Systems Principles 2009, pp. 207-220, (2009)
  • [9] Han D.S., Yang Q.L., Xing J.C., UML-Based modeling and formal verification for software self-adaptation, Ruan Jian Xue Bao/Journal of Software, 26, 4, pp. 730-746, (2015)
  • [10] Xiao D., Zhu Y.F., Liu S.L., Wang D.X., Luo Y.Q., Digital hardware design formal verification based on HOL system, Applied Mechanics & Materials, 716-717, pp. 1382-1386, (2015)
123