论文部分内容阅读
本文主要讨论仿射括号代数的算法和它在定理机器证明中的应用两方面的问题.
本文的动机有如下两个方面：
(1)括号代数作为一种崭新的定理机器证明工具已经被广泛研究，并且展示了它的强大优势.但是作为括号代数的自然扩展，仿射括号代数的相关研究却很少。无论是它的有效算法还是它在定理机器证明中的具体应用都很少有人研究.
(2)经典的无坐标定理机器证明方法主要针对射影几何和欧氏几何。有必要将仿射几何单独提出来，用仿射括号代数进行它的定理机器证明，使得无坐标方法的系统完善起来.
本文正是针对此做了大量相关工作.主要成果如下：
1.首次提出了边界扩张算法等几个有效的仿射括号代数算法，为系统实现奠定了基础.
2.讨论了仿射括号代数的展开问题和整除性问题，并给出了若干个算法.
3.完善和发展了仿射几何的构造方式以及对应表示.
4.在符号计算软件Maple 10中实现了仿射括号代数的基本算法和定理机器证明算法。在此基础上实现的系统具有如下特点：(1)能够进行仿射括号代数和括号代数的基本运算，并且能够自动化简和提取公因子。(2)程序的输入和输出完全可读，并且可以相互利用.