几何代数的高阶逻辑形式化研究

摘要

几何代数是一门关于几何的代数语言,主要用来描述、计算几何问题,目前已在几何学、理论物理学、工程应用等领域获得广泛应用.不过几何代数中的传统计算方法,如数值计算方法、符合计算法等都存在一定的缺陷.高阶逻辑则是一种严密的形式化验证方法,对于促进几何代数形式化的实用性具有重要意义.