微信服务号

微信订阅号

2025年5月1日 22:43 星期四
首页 > 过刊浏览>2016年第27卷第3期 >497-516. DOI:10.13328/j.cnki.jos.004977
PDF HTML阅读 XML下载 导出引用 引用提醒
几何代数的高阶逻辑形式化
作者:
基金项目:

国家自然科学基金(61170304,61104035,61373034,61303014,61472468,61572331);国际科技合作计划(2010DFB 10930,2011DFG13000);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)


Formalization of Geometric Algebra Theories in Higher-Order Logic
Author:
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)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [32]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等,都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后,为了说明几何代数形式化的有效性和实用性,在共形几何代数空间中,给刚体运动问题提供了一种简单有效的形式化建模与验证方法.

    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.

    参考文献
    [1] Dorst L, Lasenby CDJ. Applications of Geometric Algebra in Computer Science and Engineering. Birkhuser Boston:Springer Science & Business Media, 2002. 1-8.[doi:10.1007/978-1-4612-0089-5]
    [2] Bayro Corrochano E. Geometric Computing:for Wavelet Transforms, Robot Vision, Learning, Control and Action. Berlin:Springer-Verlag, 2010. 3-49.[doi:10.1007/978-1-84882-929-9]
    [3] Chappell JM, Drake SP, Seidel CL, Gunn LJ, Iqbal A, Allison A, Abbott. D. Geometric algebra for electrical and electronic engineers. Proc. of the IEEE, 2014,102(9):1340-1363.[doi:10.1109/JPROC.2014.2339299]
    [4] Choi HI, Lee DS, Moon HP. Clifford algebra, spin representation, and rational parameterization of curves and surfaces. Advances in Computational Mathematics, 2002,17(1-2):5-48.[doi:10.1023/A:1015294029079]
    [5] Hildenbrand D. Geometric computing in computer graphics using conformal geometric algebra. Computers & Graphics, 2005,29(5):795-803.[doi:10.1016/j.cag.2005.08.028]
    [6] Hildenbrand D, Pitt J, Koch A. Gaalop-High Performance Parallel Computing Based on Conformal Geometric Algebra. 1st ed. Springer London:Geometric Algebra Computing, 2010. 477-494.[doi:10.1007/978-1-84996-108-0_22]
    [7] Siddique U, Hasan O. On the Formalization of Gamma Function in HOL. Journal of Automated Reasoning, 2014,53(4):407-429.
    [8] Klein G, Elphinstone K, Heiser G, Andronick J, eds. seL4:Formal verification of an OS kernel. In:Matthews JN, ed. Proc. of the 22nd ACM Symp. on Operating Systems Principles 2009. Montana:ACM Press, 2009. 207-220.[doi:10.1145/1629575.1629596]
    [9] Han DS, Yang QL, Xing JC. UML-Based modeling and formal verification for software self-adaptation. Ruan Jian Xue Bao/Journal of Software, 2015,26(4):730-746(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4758.htm[doi:10.13328/j. cnki.jos.004758]
    [10] Xiao D, Zhu YF, Liu SL, Wang DX, Luo YQ. Digital hardware design formal verification based on HOL system. Applied Mechanics & Materials, 2015,716-717:1382-1386.[doi:10.4028/www.scientific.net/AMM.716-717.1382]
    [11] Resten Y, Maler O, Marcus M, Pnueli A, Shahar E. Symbolic model checking with rich assertional languages. Computer Aided Verification, 2006,43(2):424-435.[doi:10.1007/3-540-63166-6_41]
    [12] Taqdees SH, Hasan O. Formalization of laplace transform using the multivariable calculus theory of HOL-Light. In:McMillan K, ed. Proc. of the Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg:Springer-Verlag, 2013. 744-758.[doi:10.1007/978-3-642-45221-5_50]
    [13] Farooq B, Hasan O, Iqbal S. Formal kinematic analysis of the two-link planar manipulator. In:Groves L, ed. Proc. of the Formal Methods and Software Engineering. Berlin, Heidelberg:Springer-Verlag, 2013. 347-362.[doi:10.1007/978-3-642-41202-8_23]
    [14] Harrison J. 2010. https://github.com/jrh13/hol-light/blob/master/Multivariate/clifford.ml
    [15] Seung HS, Lee DD. The manifold ways of perception. Science, 2000,290(5500):2268-2269.[doi:10.1126/science.290.5500.2268]
    [16] Yuan LW, Lü GN, Luo W, Yu ZY, Yi L, Sheng YH. Geometric algebra method for multidimensionally-unified GIS computation. Chinese Science Bulletin, 2012,57(7):802-811.[doi:10.1007/s11434-011-4891-3]
    [17] Perwass C, Hildenbrand D. Aspects of geometric algebra in euclidean, projective and conformal space. Technical Report, University of Kiel, 2004. 53-67.
    [18] Li H. Conformal geometric algebra-The new theories and Computing frameworks of the geometry algebra. Computer-Aided Design & Computer Graphics, 2005,17(11):2383-2393(in Chinese with English abstract).[doi:10.3321/j.issn:1003-9775.2005. 11.001]
    [19] Harrison J. The HOL Light theory of euclidean space. Journal of Automated Reasoning, 2013,50(2):173-190.[doi:10.1007/s10817-012-9250-9]
    [20] Li H. Automated theorem proving in the homogeneous model with clifford bracket algebra. In:Dorst L, ed. Proc. of the Applications of Geometric Algebra in Computer Science & Engineering. Boston:Springer Science & Business Media, 2002. 69-78.[doi:10.1007/978-1-4612-0089-5_5]
    [21] De Sabbata V, Datta BK. Geometric Algebra and Applications to Physics. CRC Press, 2007. 21-120.
    [22] Dorst L, Fontijne D, Mann S. Geometric Algebra for Computer Science:An Object-Oriented Approach to Geometry. San Francisco:Elsevier, 2007. 204-277.
    [23] Zhang L, Zhou W, Jiao L. Complex-Valued support vector classifiers. Digital Signal Processing, 2010,20:944-955.[doi:10.1016/j.dsp.2009.09.005]
    [24] Xing Y. Research on quaternion and its applications in graphics and image processing[Ph.D. Thesis]. Hefei:Hefei University of Technology, 2009(in Chinese with English abstract).[doi:10.7666/d.y1611908]
    [25] Bayro-Corrochano E, Daniilidis K, Sommer G. Motor algebra for 3D kinematics:the case of the hand-eye calibration. Journal of Mathematical Imaging & Vision, 2000,13(2):79-100.[doi:10.1023/A:1026567812984]
    [26] Bayro-Corrochano E, Zamora-Esquivel J. Differential and inverse kinematics of robot devices using conformal geometric algebra. Robotica, 2007,25(1):43-61.[doi:10.1017/S0263574706002980]
    [27] Pham MT, Tachibana K, Yoshikawa T, Furuhashi T. A clustering method for geometric data based on approximation using conformal geometric algebra. In:Proc. of the 2011 IEEE Int'l Conf. on Fuzzy Systems(FUZZ-IEEE). 2011. 2540-2545.[doi:10.1109/FUZZY.2011.6007574]
    [28] Gull S, Lasenby A, Doran C. Imaginary numbers are not real-The geometric algebra of spacetime. Foundations of Physics, 1993, 23(9):1175-1201.[doi:10.1007/BF01883676]
    附中文参考文献:
    [9] 韩德帅,杨启亮,邢建春.一种软件自适应UML建模及其形式化验证方法.软件学报,2015,26(4):730-746. http://www.jos.org.cn/1000-9825/4758.htm[doi:10.13328/j.cnki.jos.004758]
    [18] 李洪波.共形几何代数——几何代数的新理论和计算框架.计算机辅助设计与图形学学报,2005,17(11):2383-2393.[doi:10.3321/j.issn:1003-9775.2005.11.001]
    [24] 邢燕.四元数及其在图形图像处理中的应用研究.合肥:合肥工业大学,2009.[doi:10.7666/d.y1611908]
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2015-05-24
  • 最后修改日期:2015-10-20
  • 在线发布日期: 2016-01-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号