论文部分内容阅读
【摘 要】历史上数学家在解几何中一直寻找着像解代数一样的通用公式，直到近代机器的发明，这样的系统才得以快速发展，我国数学家张景中院士以他的面积法发展起来的消点法使得机器证明几何得以实现。本文就简单介绍此法在中学几何中用纸笔解题的应用。
【关键词】几何；机器证明；消点法
在数学的历史长河中，数学家一直都希望像解代数一样为几何问题寻找一套公式，使得解几何像解代数问题一样套用公式，数学大师笛卡尔、莱布尼茨、希尔伯特等科学巨匠为此曾付出大量心血，但未能找到有效的途径。而今特别是现在电子计算机的出现，人们更希望机器能代替人类成批地解决几何问题。
电子计算机的出现，大大促进了此领域的发展，早在50年代，美国数学家阿尔弗雷德?塔斯基就用代数方法证明初等几何机械化的可能性，但直到70年代，这种方法仍未曾得到很好的发展。在这种以机器证明几何问题思维研究的发展中，我国的张景中院士以他多年来研究并发展的几何新方法（面积法）为基本工具，提出了消点法思想，并且和周咸山、高小山合作，于1992年突破了这项难题，从而实现了几何定理可读性证明的自动生成，此法不以坐标为基础，也不同于传统的综合方法，此方法以几何不变为前提，把几何、代数逻辑和人工智能方法结合起来所形成的开发系统。用最初有限的基本几何不变量与一系列作图规则并且建立有限的一系列与这些不变量和作图规则有关的消点公式，把命题的前提以作图语句的形式输入，自动化程序就可以调用相应的消点公式把结论中的约束关系逐个消去，最后得出结论，把消点的过程记录起来并且与相应的消点公式结合，就是一个具有几何意义的证明过程。
可喜的是此法亦可由人用笔在纸上执行，我们称为的消点法，消点法把证明与作图联系起来，把代数演算与几何推理密切相联，从而几何解题的逻辑性增强了，把初等几何解题从只运用四则运算的层次推进到代数方法的阶段，几何证题亦有了以不变应万变的模式。
既然消点法是在面积法的基础上发展起来的，那么下面列出消点法要用到的公式定理：
1、共边定理
有一条公共边的两个三角形，叫做共边三角形。共边三角形的面积比可以转化为线段的比。下面来介绍共边定理。
设直线AB 与直线PQ交与M，则
2、共角定理
若∠ABC和∠A’B’C’相等或互补，则有
例1 求证：平行四边形对角线相互平分。
分析 （1）任取不共线的三点A，B，C；
（2）取点D使AD//BC，DC//AB；
（3）取AC，BD的交点O；
下面是消点法的分析过程：
把图中五个点分为三组：第一组为A，B，C我们把这组的点叫做自由点，这些点不受到其它条件的约束（前提条件A、B、C不共线）。
第二组为D（此点由第一组约束产生，条件如分析（2））。
第三组为点O，有了前面四个点才有O。
我们把第一组叫做自由点，后两组叫做约束点，也就是由自由点约束产生的。这种点之间的制约关系，对解题至关重要。
要证明的结论是AO=OC，即AO：CO=1。因而解题思路是：要证明的等式左端有三个几何点A，C，O出现，右端却只有数字1，若想办法把字母A，C，O统统消掉。首先着手从式子AO：CO中消去最晚出现的点O，想消去一个点，首先得看此点的来历，以及其在何种几何量中出现。点O是由AC，BD相交而产生的，可用共边定理消去点，下一步轮到消去D，根据D的来历：AD//BC，故S△CBD=S△ABC，DC//AB，故S△ABD=S△ABC，得。
证明：由 ，即证。
例2 平行于三角形ABC的BC边的直线交三角形AB，AC边于E、D，分别连接BD，CE相于点F，AF的延长线交BC于G，求证：BG=CG。
分析：
（1）任取不共线三点ABC。
（2）在AB，AC上取点E、D，使得ED//BC。
（3）取BD、CE的交点F。
（4）取BC与AF的延长线的交点G。
于是点的关系及顺序就明确了，先有A、B、C，再有E、D，再有F，G。欲求BG=GC，只要 。根据例1可知，后出现的点一般先消去，在此式中，左边有B、C、G三点，点G是最后出现的。
于是 （G点是由BC和AF相交产生的，可利用共边定理首先消去G点。）
在上式右式中，有字母A、B、C、F。最晚出现的是F，我们想办法消去F。
由 ，
于是 （消去了点F）
又因为ED//BC，所以 ，
即
最后得 ，证毕。
从上例可以看出：题目中的条件如果可以用尺规作图表示出来，且结论可表成常用的几何量（包括面积、线段及角的三角函数）的多项式等式，就能用消点法一步一步地写出解答。如果我们想消去某点P时，首先看P是如何产生的，也就是与其它点是何种关系；二是P处在哪种几何量中，由于作图法只有有限种（设为N种），几何量也只有有限个（设为M个），故消点法方式不会超过M×N种，这就是消点法解几何题以不变应万变模式的基本依据。
收稿日期：2012-07-10
【关键词】几何；机器证明；消点法
在数学的历史长河中，数学家一直都希望像解代数一样为几何问题寻找一套公式，使得解几何像解代数问题一样套用公式，数学大师笛卡尔、莱布尼茨、希尔伯特等科学巨匠为此曾付出大量心血，但未能找到有效的途径。而今特别是现在电子计算机的出现，人们更希望机器能代替人类成批地解决几何问题。
电子计算机的出现，大大促进了此领域的发展，早在50年代，美国数学家阿尔弗雷德?塔斯基就用代数方法证明初等几何机械化的可能性，但直到70年代，这种方法仍未曾得到很好的发展。在这种以机器证明几何问题思维研究的发展中，我国的张景中院士以他多年来研究并发展的几何新方法（面积法）为基本工具，提出了消点法思想，并且和周咸山、高小山合作，于1992年突破了这项难题，从而实现了几何定理可读性证明的自动生成，此法不以坐标为基础，也不同于传统的综合方法，此方法以几何不变为前提，把几何、代数逻辑和人工智能方法结合起来所形成的开发系统。用最初有限的基本几何不变量与一系列作图规则并且建立有限的一系列与这些不变量和作图规则有关的消点公式，把命题的前提以作图语句的形式输入，自动化程序就可以调用相应的消点公式把结论中的约束关系逐个消去，最后得出结论，把消点的过程记录起来并且与相应的消点公式结合，就是一个具有几何意义的证明过程。
可喜的是此法亦可由人用笔在纸上执行，我们称为的消点法，消点法把证明与作图联系起来，把代数演算与几何推理密切相联，从而几何解题的逻辑性增强了，把初等几何解题从只运用四则运算的层次推进到代数方法的阶段，几何证题亦有了以不变应万变的模式。
既然消点法是在面积法的基础上发展起来的，那么下面列出消点法要用到的公式定理：
1、共边定理
有一条公共边的两个三角形，叫做共边三角形。共边三角形的面积比可以转化为线段的比。下面来介绍共边定理。
设直线AB 与直线PQ交与M，则
2、共角定理
若∠ABC和∠A’B’C’相等或互补，则有
例1 求证：平行四边形对角线相互平分。
分析 （1）任取不共线的三点A，B，C；
（2）取点D使AD//BC，DC//AB；
（3）取AC，BD的交点O；
下面是消点法的分析过程：
把图中五个点分为三组：第一组为A，B，C我们把这组的点叫做自由点，这些点不受到其它条件的约束（前提条件A、B、C不共线）。
第二组为D（此点由第一组约束产生，条件如分析（2））。
第三组为点O，有了前面四个点才有O。
我们把第一组叫做自由点，后两组叫做约束点，也就是由自由点约束产生的。这种点之间的制约关系，对解题至关重要。
要证明的结论是AO=OC，即AO：CO=1。因而解题思路是：要证明的等式左端有三个几何点A，C，O出现，右端却只有数字1，若想办法把字母A，C，O统统消掉。首先着手从式子AO：CO中消去最晚出现的点O，想消去一个点，首先得看此点的来历，以及其在何种几何量中出现。点O是由AC，BD相交而产生的，可用共边定理消去点，下一步轮到消去D，根据D的来历：AD//BC，故S△CBD=S△ABC，DC//AB，故S△ABD=S△ABC，得。
证明：由 ，即证。
例2 平行于三角形ABC的BC边的直线交三角形AB，AC边于E、D，分别连接BD，CE相于点F，AF的延长线交BC于G，求证：BG=CG。
分析：
（1）任取不共线三点ABC。
（2）在AB，AC上取点E、D，使得ED//BC。
（3）取BD、CE的交点F。
（4）取BC与AF的延长线的交点G。
于是点的关系及顺序就明确了，先有A、B、C，再有E、D，再有F，G。欲求BG=GC，只要 。根据例1可知，后出现的点一般先消去，在此式中，左边有B、C、G三点，点G是最后出现的。
于是 （G点是由BC和AF相交产生的，可利用共边定理首先消去G点。）
在上式右式中，有字母A、B、C、F。最晚出现的是F，我们想办法消去F。
由 ，
于是 （消去了点F）
又因为ED//BC，所以 ，
即
最后得 ，证毕。
从上例可以看出：题目中的条件如果可以用尺规作图表示出来，且结论可表成常用的几何量（包括面积、线段及角的三角函数）的多项式等式，就能用消点法一步一步地写出解答。如果我们想消去某点P时，首先看P是如何产生的，也就是与其它点是何种关系；二是P处在哪种几何量中，由于作图法只有有限种（设为N种），几何量也只有有限个（设为M个），故消点法方式不会超过M×N种，这就是消点法解几何题以不变应万变模式的基本依据。
收稿日期：2012-07-10