马莎

作品数：2被引量：6H指数：2
导出分析报告
供职机构：首都师范大学更多>>
发文主题：共形几何代数HOL形式化验证定理证明形式化分析方法更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《小型微型计算机系统》《软件学报》更多>>
所获基金：国际科技合作与交流专项项目国家自然科学基金北京市教委科学研究与科研基地建设项目北京市科委项目更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-2
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
几何代数的高阶逻辑形式化被引量：5
《软件学报》2016年第3期497-516,共20页马莎 施智平 李黎明 关永 张杰 Xiaoyu SONG 
国家自然科学基金(61170304;61104035;61373034;61303014;61472468;61572331);国际科技合作计划(2010DFB10930;2011DFG13000);北京市科委项目(Z141100002014001);北京市教委科研基地建设项目(TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划(IDHT20150507)~~
几何代数是一种用于描述和计算几何问题的代数语言,由于它统一表达分析和不依赖于坐标的几何计算等优点,现已成为数学分析、理论物理、几何学、工程应用等领域重要的理论基础和计算工具.然而,利用几何代数进行计算和建模分析的传统方法...
关键词：几何代数 形式化验证 定理证明 HOL-Light 几何积 
共形几何代数与机器人运动学的形式化被引量：3
《小型微型计算机系统》2016年第3期555-561,共7页马莎 施智平 关永 李黎明 邵振洲 张杰 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目;北京市属高校青年拔尖人才培育计划资助
共形几何代数作为一种新的几何表示和计算系统,它为经典几何提供了简洁、直观和统一的齐性代数框架,目前在现代科技的各个领域有很广泛的应用,但是利用共形几何代数进行计算和建模分析的传统方法如数值计算方法和符号方法存在计算不精...
关键词：共形几何代数 形式化验证 定理证明 HOL-Light 运动学反解 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部