微信服务号

微信订阅号

2025-4-21- 11
Home > Archive>Volume 27, Issue 3, 2016 >497-516. DOI:10.13328/j.cnki.jos.004977
PDF HTML XML Export Cite reminder
Formalization of Geometric Algebra Theories in Higher-Order Logic
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61170304, 61104035, 61373034, 61303014, 61472468, 61572331); Int’l Cooperation Program on Science and Technology (2010DFB10930, 2011DFG13000); Beijing Municipal Science and technology project (Z141100002014001); Scientific Research Base Development Program of the Beijing Municipal Commission of Education (TJSHG201310028014); Project of Construction of Innovative Teams and Teacher Career Development for Universities and Colleges under Beijing Municipality (IDHT20150507)

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

马莎,施智平,李黎明,关永,张杰,Xiaoyu SONG.几何代数的高阶逻辑形式化.软件学报,2016,27(3):497-516

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:May 24,2015
  • Revised:October 20,2015
  • Online: January 06,2016
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063