主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
马莎,施智平,李黎明,关永,张杰,Xiaoyu SONG.几何代数的高阶逻辑形式化.软件学报,2016,27(3):497-516
几何代数的高阶逻辑形式化
Formalization of Geometric Algebra Theories in Higher-Order Logic
投稿时间:2015-05-24  修订日期:2015-10-20
DOI:10.13328/j.cnki.jos.004977
中文关键词:  几何代数  形式化验证  定理证明  HOL-Light  几何积
英文关键词:geometric algebra  formal verification  theorem proving  HOL-Light  geometric product
基金项目:国家自然科学基金(61170304,61104035,61373034,61303014,61472468,61572331);国际科技合作计划(2010DFB 10930,2011DFG13000);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)
作者单位E-mail
马莎 轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048
首都师范大学成像技术北京市高精尖创新中心, 北京 100048 
 
施智平 轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048
北京数学与信息交叉科学2011协同创新中心, 北京 100048 
zhizp@cnu.edu.cn 
李黎明 轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048  
关永 轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 100048
北京数学与信息交叉科学2011协同创新中心, 北京 100048 
 
张杰 北京化工大学信息科学与技术学院, 北京 100029  
Xiaoyu SONG Electrical and Computer Engineering, Portland State University, Portland, USA  
摘要点击次数: 2557
全文下载次数: 1805
中文摘要:
      几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法,如数值计算方法和符号方法等,都存在计算不精确或者不完备等问题.高阶逻辑定理证明是验证系统正确的一种严密的形式化方法.在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型,主要包括片积、多重矢量、外积、内积、几何积、几何逆、对偶、基矢量运算和变换算子等的形式化定义和相关性质定理的证明.最后,为了说明几何代数形式化的有效性和实用性,在共形几何代数空间中,给刚体运动问题提供了一种简单有效的形式化建模与验证方法.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利