对简易几何机械化证明的进一步研究

对简易几何机械化证明的进一步研究第1页

对简易几何机械化证明的进一步研究
南京航空航天大学 040630520 彭立勋

关键字：机械化证明搜索比对方案
项目摘要：
“机械化证明”，就是用计算机进行判断、推理、证明等活动的集合。做这个课题的关键，就在于如何利用
计算机模拟出人脑的推理过程。我采用的思维方式，
即：归纳-->演绎-->推理的思维过程。所以，整个搜索系统由以下三大部分组成：
1.知识库：包括当前证明所需的全部公式定理。
2.扩展规则：控制节点扩展的方案。作用于当前一个节点，产生其后继节点。
3.控制策略：控制节点中信息与知识库之间的对比，测试是否已证到需证结论或得出无法证明。
然后建立一个 Con 函数，用信息的 Def 值为参数，生成 Con 地址，填入 Con 表中，在搜
索对比时只要查询 Con 表的地址，就可以知道是否有相同信息，大大加快搜索效率。（Con 函
数，Con 表, Con 地址，Def 值的含义见论文）
关键更新：Con 表存储结构。

“人工智能学”就是智能机器所执行的通常与人类智能有关的功能，如判断、推理、证明、识别、感知、理
解、设计、思考、规划、学习和问题求解等思维活动。实现人工智能，有两种方法，一是在硬件上，一是在软件
上。用硬件方法就是做出仿生物处理器，让处理器的运行模拟人脑的运行模式，但是就目前的现实来看，生物处
理器在短时间内不可能被制造出来。所以就目前而言，我们只能靠软件的方法，也就是用程序来模拟人脑的思维
方式，来实现人工智能。
机械化证明，是人工智能学的一个分支，是判断、推理、证明等活动的集合，即从计算机外部输入已知条件
和需要证明的结果，再通过计算机模拟人脑进行“推理”，判断出通过已知条件是否可以得到我们要证明的结论
或者给出证明步骤。
清华大学吴文俊教授曾经成功的完成过一个机械化证明程序，提出了“吴氏算法”，可以证明欧拉几何、平
面几何等问题，但是吴文俊教授的设计思想比较复杂复杂，主要从数学方面入手，而不是从人脑的思维方式入手，
所以需要很深的数学知识才能理解。此外还有面积法，坐标法等机械化证明方法，但这些算法也和吴文俊教授差
不多，都不是主要从人脑的思维方式入手，偏向数学方法，不是大部分人可以理解的。
我对吴教授的算法专门研究过一段时间，可是基本没有明白吴文俊教授的设计思想，因为其方法涉及的知识
太深太广，理解难度相当大，非普遍可以理解的算法。所以我决定设计一套易于理解，有一定实用价值的机械化
证明算法，“简单的几何问题”证明就是第一步。所谓“简单几何证明”，就是可以不作辅助线通过定理直接做出
来的几何证明题（本文仅以高二数学几何证明内容为例具体说明）。
对这个课题，我提出了一个个算法，又不断的发现错误和提出提高效率的方法，进行修改。经过多次的修正，
我最终研究出了一套“Con 函数+Con 表+Con 地址（Con 函数/Con 表/Con 地址后文有详细说明）
”的方法，还比较可行。
做这个课题的关键，也是难点之处，就在于如何利用计算机模拟出人脑的推理过程。

因此，首先必须对大脑的思维过程有一定的认识。人的思维过程：。归纳，就是从一
系列个别的、特殊的前提，推出一般的、普遍性的结论的过程。对于归纳来说，前提与结论之间的联系是或然性
的，其结论的真实性必须由实践来论证。而演绎，就是由一般的、普遍性的前提提出个别的、特殊性的结论的过
程，从某种意义上说，演绎就是归纳的特定条件下的还原。对于演绎来说，前提与结论的关系是必然的，也就说，
只要前提正确，推出的结论一定正确。然后推理，就是由若干个已有的判断得出另一个新的判断过程。完成推理
后，会得出一个新的判断，根据这些判断，又可以归纳出新的结论。接着，又开始新一轮的归纳、演绎、推理之

1


间的循环，这就是人思维积累、学习知识，不断提高自身智慧的过程。
而人们进行证明，当然也是这个思维过程。人们首先根据以往归纳的经验（包括题型的固定解题思路，公式
定理等）确定此问题的类型，判断大致思路，然后根据题目的实际条件在一定范围内进行演绎，修改硬套的解题
思路，摸索符合实际情况的解题方法，同时搜索大脑里的对定理公式的记忆，调用其中相关的（即有可能使用到
的）公式定理，与本问题已知条件进行对比，然后推理出本题的解题思路，得出证明步骤或一些结论结论。
根据这些简单的分析，大致模拟上面分析的过程，就可以初步建立起证明程序的计算机算法模型。
于是，一开始我很自然地想到用“广度优先搜索”和“深度优先搜索”，以及“双向搜索”等搜索方法为核
心，佐以合理的数据结构，加以一定的剪枝优化来编写程序。
为了能够让计算机“明白”要用到的公式定理，首先必须建立一个完备的知识库，知识库中包含了证明所需
的“知识”——计算机能够识别的按一定格式储存的公式定理数据库。然后，在搜索的时候，需要根据搜索知识
库的情况，扩展一些条件节点。所以必须有一个扩展规则来作用于一个节点，产生其后继节点使搜索能够进行下
去。此外，还需要一个控制策略，来控制搜索的过程和方案，以及测试是否达到终止条件（包括达到需证结论、
得出无法证明或满足用户自定义的终止条件），记录扩展信息等。
所以，整个搜索系统由以下三大部分组成：
1.知识库：包括当前证明所需的全部公式定理。可以在程序中内置完整的知识库，也可以通过数据库的
形式从程序外部提供。
2.扩展规则：控制节点扩展的方案。作用于当前一个节点，产生其后继节点。
3.控制策略：控制节点中信息与知识库之间的对比，测试是否已证到需证结论或得出无法证明或满足用户
自定义的终止条件，记录节点扩展时产生的信息。
由于进行搜索时，必须要有统一的数据记录形式，才能完成搜索，而用户输入的条件不一定按照程序定义的
数据结构来输入，因为为了方便处理，程序使用的数据结构都比较复杂，所以还应该建立一个格式化系统，来对
用户输入的一般格式的条件、知识库等进行格式化处理，储存为程序运算储存使用的格式。
根据这些组成部分及其作用，我提出了如下的算法框架（包括算法说明图）：
（本文中出现的程序代码全部为 Pascal 语言代码，知识库本文中用 Text 文本格式来说明。但在实际应用中应
使用 Delphi/C/C++语言配合数据库来实现）
{ 1.读入已知条件及需证结论。
2.判断用户是否提供知识库。
3.1.如果用户提供数据库，格式化已知条件、需证结论以及用户提供的外部数据库；
3.2.如果用户不提供数据库，格式化已知条件、需证结论，初始化程序内置知识库或外部自带的数据库。
4.按控制策略开始搜索知识库，对比已知条件。
5.按扩展规则扩展当前节点。
6.按控制策略判断是否满足终止条件。
7.1.如果满足终止条件则输出结果，结束程序；
7.2.如果不满足终止条件则转(4)继续搜索。
}

为放源程序，故删去图片使文件小于 100K
（算法说明图）
为了便于程序编写，便于计算机识别数据，可以把一些数据类型、数学符号、图形类型以及标识字母进行了
编号（本文我仅对高二数学几何证明出现的相关内容进行编号），并称其编号为此数据或数据类型的
Def（Definition，定义）值，这样在程序中可以更方便地判断数据类型，也利于本文的论述说明。
{ 附 Def 值表：
参数数据类型编号

2


参数数据类型点参数线参数平面参数体、空间参数符号参数
编号 0 1 2 3 4
考虑/适用范围编号
适用范围只考虑/适用平面几何
/ 只考虑/适用空间几何
/ 平面空间几何都考虑/适用
/
编号 1 2 3
平面图形类型编号
图形类型(梯形)
( ) 未定类型梯形斜梯形直角梯形
编号 210 211 212
图形类型(四边形)
( ) 未定类/普通平行四边形
/ 矩形正方形菱形
编号 220 221 222 223
图形类型(三角形)
( ) 未定类型三角斜三角形正三角形锐角三角形钝角三角形直角三角形
形
编号 230 231 232 233 234 235
图形类型(圆形)
( ) 未定圆类图形正圆椭圆
编号 240 241 242
图形类型(多边形)
( ) 未定多边形正多边形非正多边形
编号 250 251 252
空间图形类型编号
图形类型棱柱棱锥圆柱球正多面体
编号 310 320 330 340 350
具体类型正棱斜棱正棱斜棱正圆斜圆球体四面六面八面十二二十
柱柱锥锥柱柱面面
编号 310 311 321 322 331 332 340 351 352 353 354 355
数学符号编号
数学符号 ∈ （无）（无）＝

意义属于不属于包含与不包含于平行垂直异面相交等于

编号 1 2 3 4 5 6 7 8 9

标识字母编号
标识字母 ‘A’～‘Z’
A Z ‘a’～‘z’
a z
编号 10～35（Ord('A') 55～Ord('Z') 55）
3 Ord('A')
Ord('A')－5 Ord('Z')
Ord('Z')－5 36～61（Ord('a') 61 Ord('z') 61
6 Ord('a') 61～Ord('z') 61）
Ord('a')－61 Ord('z')－61
}
有了上面定义的编号（Def 值），计算机就可以在处理数据时，通过扫描编号来判断或得知数据的类型，从
而缩小题目中考虑的范围，例如是否考虑空间几何，有关于没有垂直、平行的条件或须证结论等等。这样可以只
搜索知识库中可能用到的公式定理，例如题目不考虑空间几何则根本不需要搜索立体几何数据库。这样可以减少
大量无谓的搜索，在很大程度上提高搜索的效率。否则，在不知道数据类型的情况下进行盲目搜索，且不说其产
生大量垃圾节点降低搜索效率的坏处，单立体几何与平面几何就有不少条件相同但结论不同的定理，例如 a b、
b c，在平面几何里可以推出 a//c 的结论，但是立体几何中 a、c 可能异面垂直可能平行还可能就是异面直线，
这是完全不同的结论。因此，用编号来描述数据类型不仅可以提高搜索效率，还可以避免错解的发生。
接着，为了方便对搜索时的信息进行处理，必须建立合理的数据结构。
所谓合理地数据结构，首先，要能准确无误的表达出问题描述的信息、每一步搜索的具体情况；然后，要能
够使程序方便地得知目前证明中全局进行的状况，；最后，还要顾及数据所占用的空间，把空间占用控制在大部

3


分主流计算机比较容易承受的范围之内。
经过思考和尝试，我首先确定了如下的输入文件（包括已知条件和需证结论，知识库）的数据结构，用户可
以按这个结构输入题目的信息和自建知识库。
{ 输入信息数据结构：
已知条件和需证结论标准格式：
[ 第 1 行：有几种参数 N 已知条件数需证结论数几种符号考虑范围（均为 Byte 类型）
第 2 行：参数类型 1 参数类型 1 数目（均为 Byte 类型）参数表（String[52]类型）
……
第(1+N)行：参数类型 N 参数类型 N 数目（均为 Byte 类型）参数表（String[52]类型）
第(2+N)行：已知条件 1.已知条件 2.…….已知条件 M.（均为 String[5]类型，用'.'分开每个条件，符号用 DEF 值）
第(3+N)行：需证结论 1.需证结论 2.…….需证结论 M.（均为 String[5]类型，，用 '.'分开每个结论，符号用 DEF 值） ]
例如，条件为“有直线 a,b,c，已知 a//b,b//c”，要证“a//c”，表示成上面的数据结构就是：
[ 第 1 行：1（表示有一种参数类型） 2（表示有 2 个已知条件） 1（表示有 1 个需证结论） 1（表示只有 1 种符号） 1（只
考虑平面几何）
第 2 行：1（表示线类型参数） 3（表示有 3 个线类型参数） abc（有 a,b,c 这 3 个线型参数）。
第 3 行：a6b.b6c.（两个已知条件 a//b 和 b//c）
第 4 行：a6c. ]
知识库标准格式：
每条定理的输入格式
[ 第 1 行：有几种参数 N 充分条件数可得结论数几种符号适用范围（均为 Byte 类型）
第 2 行：参数类型 1 参数类型 1 数目（均为 Byte 类型）参数表（String[52]类型）
……
第(1+N)行：参数类型 N 参数类型 N 数目（均为 Byte 类型）参数表（String[52]类型）
第(2+N)行：充分条件 1.充分条件 2.…….充分条件 M.（均为 String[5]类型，用'.'分开每个条件，符号用 DEF 值）
第(3+N)行：可得结论 1.可得结论 2.…….可得结论 M.（均为 String[5]类型，用'.'分开每个结论，符号用 DEF 值）
第(3+N)行：空行 ]
例如，定理“在空间或平面中直线 a//直线 b，直线 b//直线 c，则直线 a//直线 c”，表示成上面的数据结构就是：
[ 第 1 行：1（表示有一种参数类型） 2（表示有 2 个充分条件） 1（表示有 1 个可得结论） 1（表示只有 1 种符号） 3（平
面/立体几何都适用）
第 2 行：1（表示线类型参数） 3（表示有 3 个线类型参数） abc（有 a,b,c 这 3 个线型参数）。
第 3 行：a6b.b6c.（两个已知条件 a//b 和 b//c）
第 4 行：a6c.
第 5 行：（空） ]
}
当读到有（平面/空间）图形的数据时，应该在读取完所有数据之后，把图形转化成由图形可得的信息，例
如：到
读 “222 ABCD”（正方形 ABCD）就在数据全部读完后把这条信息转成
， “直线 AB 平行 CD、BC 平行 AD、AB
垂直 BC、BC 垂直 CD、CD 垂直 DA”等条件，并且保存。但是目前我们定义的标识符只有 52 个大小写英文字
母，一个字母代表一个数据，为了储存 AB,BC,CD,DA，可以从还未使用的字母中选出 4 个来代替它们。像
Ch:Array[‘A’..’z’]Of String 这样的数据结构就可来储存哪些标识符可用及已用的标识符代替的是什么。比如
当’A’标识符还未使用时，Ch[‘A’]=’’；当’A’标识符代表题中的 AB 时，则 Ch[‘A’]=’AB’。
然后就必须考虑如何来建立中间节点的数据结构和储存方式、以及与知识库对比的方式。如果采取直接记录
法，即用字符串形式直接记录下定理公式，保存在节点里。这种储存方式虽然直接明了，但是与知识库或逆向节

4


点对比时就只能采用把节点里的条件全排列组合，个条件生成
N + +……+ 种排列，再与知识库或逆向节

点对比。因此这种方式必然会导致比较效率低下，以至于达到比 N^M 还糟糕的时间时间复杂度，这是相当可怕
的。比如正向有 100 个节点，逆向有 100 个节点，正逆向节点对比次数就会达到 100×100＝10^4 次，如果知识
库中又有 100 条定理，那么正逆向节点与知识库对比又多达 2×10^4 次，这一次扩展总共就对比了 4 万次；而正
向如果达到 1×10^5 个节点，反向也达到 1×10^5 个节点，这样仅一次正逆节点对比次数就达到 1×10^10 次之
多！何况，这还没有考虑其他运算的时间。而且，节点多，扩展时与数据库对比次数也是指数级上升，这样的算
法和数据结构其时间效率将会相当可怕！然而，在实际中，即使证明一些普通的题目，其证明也很容易就可以达
到几十步、上百步，N^(a*10^1)～N^(a*10^2)的的时间效率显然是不能忍受的。因此，提出更好的中间储存方式、
更好的对比方式以达到减少节点，减少比较次数的目的，是最关键的问题。
通过观察证明的特性，可以发现这样一个特点：从正向推理，每次推理出的新结论，可以和原有的条件合在
一起当作下一步证明的已知条件继续往下推理。例如已知 a//b、b//c、c//d，其中 a//b 和 b//c 可以推出 a//c，a//c
和 c//d 又可以推出 a//d。但是，从反向推理，结论的充分条件完全可以推出结论本身，而不需要和结论合在一起
生成一个新节点进行对比，也许有多套充分条件可以推出一个结论，只要满足其中一套充分条件就可以推出结论。
例如 a//b 和 b//c 可以推出 a//c，a b 和 c b 在平面几何也可以推出 a//c，但只要满足 a//b、b//c 或在平面几何中
a b、c b 两个中的一个，就可以推出 a//c，而不需要两套都满足。
由于证明的这个特殊性，从正向搜索和从逆向搜索的扩展策略就有一定的区别。顺序证明由于用过的条件可
以和新推出的结论一起使用推出新的结论，所以计算机正向搜索的扩展策略可以只在原节点基础上不断添加信息
即可。而从结论反推，可能有几条思路都可以到达结论。所以，逆向搜索的扩展策略是每次反推出的结论的充分
条件都要用一个新节点来保存。因此控制策略中只要某时刻搜索中逆向搜索出的某一节点中的信息在正向搜索的
节点中都能找到，即满足了一个终止条件则认为证明成功。

（机械化证明几何问题的算法模型简图）

于是，我决定建立一个固定大小带有 Boolean 变量域的表（Com=Array[起始值..终点值] Of Data）用来储
存正向搜索的节点信息并作为对比表，称之为 Con（Contrast 比较）表，其地址称之为 Con 地址，初始化 Boolean
变量域为 False。而逆向用数组指针来存储（即数组+指针，如 Dat=Array[1..100] of ^List）。这样，正向节点每
一条信息就产生一个唯一的地址，把表中此地址的 Boolean 变量域的值赋为 True，通过查一次表，就可以判断是

5


否有相同信息。但是通过实践，逆向搜索很多时候反而会降低效率，因为逆向搜索节点数量不断膨胀，搜索次数
增加，还不如只有正向搜索，于是我决定只采取正向搜索。
现在，关键问题到了如何使一条信息只生成一个唯一的地址。因为只有这样，对照时，同样的信息才能产生
同样的地址，所以对比时只要此地址的 Boolean 域值为 True 则说明有相同的一条信息，如为 False 则说明没有相
同的一条信息。
如何使不同的信息生成唯一的地址，同时又能节省空间，节省时间，我尝试了不少方案。例如线性函数。
但是都或多或少有些毛病。通过试验，综合时间效率和空间效率，我采用了一种最简单的方案：对于一个条件，
我取其 Def 值，转化为字符串进行加运算，生成一个新字符串，把这个字符串转化为数字即为这条信息的 Con
地址。例如，"a b"这个条件，"a"的 Def 值为 37，" "的 Def 值为 6，"b"的 Def 值为 38，则生成的 Con 地址字
符串为"37"+"6"+"38"="37638"，转化为整形数据 37638 即为"a b"这条信息的 Con 地址。由于同一个符号的两边
的字符若相同，其生成的地址必然相同。但是"a b"和"b a"实际是等价的条件，但是它们的 Con 地址却一个是
37638，一个是 38637，这是两个不同的 Con 地址。
为了解决这个问题，我提出了两个方法，一是生成 Con 地址时可把另一个对应等价条件的 Con 地址赋为 True，
因为等价条件的 Con 地址是对称的，知道一个肯定可以推出另一个。二是生成 Con 地址时，把 Def 值小的放前
面，比如"a b"生成的 Con 地址为 63738，这样第一个数字表示符号，后面 4 个数字每两个表示一个字母，这样
生成的 Con 地址必然是最小的，所以也唯一。
但是无论哪种方法，储存直接生成的 Con 值都有空间浪费，例如：63163。为了减小储存时的空间浪费，我
采取了三维数组的方法，把 Con 地址的分成 3 个部分：左标识符部分，符号部分，右标识符部分。左标识符部
分储存左标识符可能的范围，符号部分部分储存符号部分可能的范围，右标识符部分储存右标识符可能的范围。
那么，第一种方法 Con 表的 Con 地址从[11,1,12]（"A∈B"）到[62,9,61]（"z=y"，z＝y）共 23400 个数据，
，
而直接储存 5 位数的 Con 地址则有 51850 个数据，可见空间效率提高了一半。第二种方法 Con 表的 Con 地址从
[1,11,12]（"A∈B"）到[9,61,62]（z＝y）共 23409 个数据，而直接储存 5 位数的 Con 地址则有 85051 个数据，
，
空间效率提高更加明显。
两种方法操作次数相近，优化储存方式后，第一种方法数据量稍微小一点，而且一些特殊情况第二种方法还
会出错，例如： “点 b 属于直线 a”，用第二种方法生成的地址可能被认为是“直线 a 属于点 b”,虽然对证明结果
影响不大，但是输出的证明步骤，可能就会出错。显然第一种方法更优秀，于是应该采用第一种方法。
还有一种特殊情况，就是 A∩B=c 的情况，这种情况有三个字母，所以按上面的方法，可以另外生成一张表，
地址从[11,12,13]（"A∩B=C"）到[62,61,60]（"z∩y=x"），对比时单独判断这张表即可。
但是还有一种方法，可以只开一张 Con 表。就是储存的时候，把"A∩B=C"形式的信息换成 3 个等价信息：A
属于或包含于 C、B 属于或包含于 C、A 相交于 B，储存在 Con 表中。我推荐使用此种方法，因为这个方法可以
节省大量空间（另开一张表专门存此类数据，要开 124800 个元素的数组），还可以编程变成复杂度（只对比一张
表总比对比两张表容易）。
为了能够倒推出证明步骤，还必须在 Con 表上加上一个域，用来储存某个 Con 地址所表达的信息的充分条
件的 Con 地址，这样在证明时就可逆推出全部的证明步骤。
其实，进一步研究可以发现，两个元素（点、线、面）之间最多存在两种关系，例如异面垂直（异面和垂直
两重关系）。所以开一个三维数组显然还是浪费了许多空间，其实我们只要开一个二维数组存下两个元素之间的
对应关系即可，也就是说用“Con:Array[元素下界..元素上界，元素下界]Of 对应关系”记录元素之间的关系。那
么对于两重关系的元素，只要在[A,B]上赋值第一种关系，在[B,A]上赋值第二种关系即可，这样空间利用就达到
了最大化。
在对比的过程中，还有许多的剪枝可以用到，这样可以减少无谓的搜索。比如：当某条定理的适用范围不包
括我们要证的问题的考虑范围，则根本不需要去对比这条定理；当某条定理条件中的参数数量大于我们已用的参
数数量时，不需要对比这条定理；当某条定理条件中的数学符号数量大于我们已用的数学符号数量时，不需要对
比这条定理；当某条定理条件中的某种类型参数数量大于已知的这种类型参数数量时，不需要对比这条定理；如

6


果把定理都搜索了一遍，没有任何结论可以推出，则这个结论不可能用已知的知识库证明出来，输出不可证……
此外知识库的对比时，数据库用的标识符很可能与题中的不一致，所以要将定理中的标识符与已用的标识符
进行替换，再进行对比。假设目前对比的定理中，点参数有 N1 个，线参数有 N2 个，面参数有 N3 个，已知的
所有条件中，点参数有 M1 个，线参数有 M2 个，面参数有 M3 个，方法是：从已用的点参数标识符 M1 个中取
出 N1 个，进行全排；从已用的线参数标识符 M2 个中取出 N2 个，进行全排；从已用的线参数标识符 M3 个中
取出 N3 个，进行全排；然后将每一种排列情况排列出的标识符序列与定理的标识符替换，进行对比。
然后判断是否可以得出结论，若可以得出结论，则判断这个推出的结论的 Con 地址是否是要证的结论，如
果是，则停止证明，输出可证和证明步骤，如果不是我们最终要的结论，则把结论存入 Con 表。接着再对比下
一条结论。
总结我的证明策略，就是利用一个函数，把信息生成一个地址，然后用一张表，存下全部可能出现的地址，
然后证明时，已知的信息，则生成地址，填在表中的这个地址。直到要证的结论生成的地址被填到时，就可以认
为证明成功，然后倒推出每一步证明步骤。

（参考过的信息：《实用算法设计》吴文虎著，清华大学有关人工智能的课件）

程序：
{$H+}
Program AI_Math_Prove;

Uses
Classes, SysUtils;

Const
MinCa=11;MaxCa=62;
MinCb=1;MaxCb=9;
MinCc=12;MaxCc=61;
Max=255;
{=================================数据结构==================================}
Type
TChar=Record
Num:Byte; //符号的 Def 值
Lab:Char; //符号的标识符
End;
TParameter=Array[0..4]Of String;//数据类型
TPlane=Array[210..252]Of String;//平面图形类型
TSolid=Array[310..355]Of String;//立体图形类型
TMark=Array['1'..'9']Of TChar; //运算符
TLabel=Array['A'..'z']Of Byte; //标识符
DefNum=Record //Def 值
Parameter:TParameter;
Plane:TPlane;
Solid:TSolid;
Mark: TMark;

7


Lable:TLabel;
End;
RConAdr=Record
N1,N2,N3:Byte;
End;
TBool=0..2;//0 表示未填，1 表示已填，2 表示是结论地址
TUp=Array[1..Max]Of ^RConAdr;
RCon=Record
Up:TUp; //推出此信息的充分条件的 Con 地址
Num:Byte; //有多少个充分条件
Flag:TBool; //是否被填写
End;
TCon=Array[MinCa..MaxCa,MinCb..MaxCb,MinCc..MaxCc]Of ^RCon;//Con 表结构
TFileName=Record //输入输出，知识库文件名
Flag:Boolean;
Inn,Outn,Datan:String;//输入、输出、知识库文件名
End;
RUsed=Record
Flag:Boolean;//是否被用
Kind:Byte; //标识符的数据类型
End;
TUsed=Array['A'..'z']Of RUsed;
TNowCan=Array[0..3,1..52]Of Char;
TSetCh=Set Of Char;
RParam=Record //参数
ParamCh:String; //有哪些标识符
Param:Array['A'..'z']Of String; //原来地标识符现在代表什么
Num:Byte; //此类参数数目
End;
RMark=Record
MarkN:Array['1'..'9']Of Byte; //符号出现多少次
Kind:Byte; //多少种符号
End;
TParamI=Array[0..3]Of RParam;
TInf=Record //全局信息
Used:TUsed; //哪些表标识符已经用过
MarkI:RMark; //运算符号信息
Lable:TLabel; //标识符的类型
ParamI:TParamI; //每种类型数据的信息
MarkSet:TSetCh; //单项运算符集合
ThN,Left:Byte; //一共调用了多少条定理和还剩多少结论未证
Step,StepN:Byte; //进行了多少步证明
Scope,Total:Byte; //考虑范围和参数总数

8


CondN,CondK,ResN:Byte; //已知条件数和有几种参数以及需证结论数
Can:Array[1..9]Of TSetCh; //参与某一运算符的标识
End;
STheorem=Array[1..Max]Of ^String[5];
RTheorem=Record //一条定理的信息
MarkI:RMark; //运算符号信息
ParamI:TParamI; //参数表
Cond,Res:STheorem; //条件和结论的储存表
Can:Array[1..9]Of TSetCh; //参与某一运算符的标识
CondN,CondK,ResN,Scope:Byte;//参数数目,有几种参数,有几个结论,考虑范围
End;
TTheorem=Array[1..Max]Of ^RTheorem;//定理存储表
TResCon=Array[1..Max]Of ^RConAdr; //需证结论的 Con 地址储存表
TConData=Array[1..3,1..3]Of Byte; //临时储存 Con 地址

Var
Fl:Text; //文件变量
Con:TCon; //Con 表
Inf:TInf; //全局信息
Def:DefNum; //Def 值表
Fn:TFileName; //文件名信息
ResCon:TResCon; //结论的 Con 地址表
Theorem:TTheorem; //公式定理记录表

{================================Procedure Init=============================}
Procedure Init;
Var I,J,K:Word;L:Char;
Begin
With Inf Do
Begin
Step:=0;
MarkSet:=['{','}','[',']'];
For I:=0 To 3 Do
Inf.ParamI[I].Num:=0;
For I:=1 to 9 Do Can[i]:=[];
For L:='1' To '9' Do MarkI.MarkN[L]:=0;
End;
For L:='A' To 'z' Do Inf.Used[L].Flag:=False;
For I:=MinCb to MaxCb Do
For J:=MinCc to MaxCc Do
For K:=MinCa to MaxCa Do
Begin
Con[K,I,J].Flag:=0;//初始化 Con 表 Boolean 域为假

9


Con[K,I,J].Num:=0;
End;
With Def Do
Begin
For L:= 'A' to 'Z' Do Lable[L]:=Ord(L)-54;
For L:= 'a' to 'z' Do Lable[L]:=Ord(L)-76;
Mark['1'].Lab:='属于';Mark['1'].Num:=1;
Mark['2'].Lab:='不属于';Mark['2'].Num:=2;
Mark['3'].Lab:='包含于';Mark['3'].Num:=3;
Mark['4'].Lab:='不包含于';Mark['4'].Num:=4;
Mark['5'].Lab:='平行';Mark['5'].Num:=5;
Mark['6'].Lab:='垂直';Mark['6'].Num:=6;
Mark['7'].Lab:='异面';Mark['7'].Num:=7;
Mark['8'].Lab:='相交';Mark['8'].Num:=8;
Mark['9'].Lab:='=等于';Mark['9'].Num:=9;
End;
End;

{=============================Procedure Con==============================}
Procedure MakeCon(St:String;Var A:TConData);
Var Len:Byte;
Begin
Len:=Length(St);
If Len=3
Then Begin
A[1,1]:=Def.Lable[St[1]];
A[1,2]:=Def.Mark[St[2]].Num;
End
Else Begin
A[1,2]:=8;
If Inf.Lable[St[5]]=0
Then Begin A[2,2]:=1;A[3,2]:=1;End
Else Begin A[2,2]:=3;A[3,2]:=3;End;
End;
End;

10


{============================Procedure Print=============================}
Procedure Print(St:String[5];IsOK:Boolean);
Var Adr:TConData;Tmp:Rcon;Ad:RConAdr;I,J,N:Byte;
Begin
If (Not IsOK)
Then Writeln(Fl,'结论',St,'在',Inf.StepN,'步之内无法证明!')
Else Begin
MakeCon(St,Adr);
Dec(Inf.Left);
WritelN(Fl,St[1]+Def.Mark[St[2]].Lab+St[3],'已经被证!');
End;
End;

{==============================Procedure CheckWork=======================}
Procedure CheckWork(N:Byte);
VAR DB:Array['A'..'z']Of Char;//标识符替换表
A,B:Array[1..10] of Byte;
C,D:Array[1..10] of Boolean;
I,J:Byte;Ch:Char;
Now1,Now2:TNowCan; //记录全局和定理中用到的标识符
Tmp,Stp:String;
Adr:TConData;
YN:Boolean; //次定理是否可推出信息
Link:TUp;

Procedure ZuHe(N1,M1,L1:Byte);
Var i,j:Byte;
Procedure Check;
Var I,L:Byte;
Begin
For I:=1 To M1 Do DB[Now2[L1,i]]:=Now1[L1,B[i]];
If L1=3 Then Begin
YN:=True;I:=0;J:=0;
While (YN)And(I<Theorem[N]^.CondN) Do
Begin
Inc(I);
Stp:=Theorem[N]^.Cond[I]^;
If Length(Stp)=3
Then Begin
Tmp:=DB[Stp[1]]+Stp[2]+DB[Stp[3]];
MakeCon(Tmp,Adr);
If (Con[Adr[1,1],Adr[1,2],Adr[1,3]]=Nil)
Then YN:=False

11


Else Begin
Inc(J);New(Link[J]);
Link[J]^.N1:=Adr[1,1];
End{If Else}
End{Then}
Else Begin
Tmp:=DB[Stp[1]]+Stp[2]+DB[Stp[3]]+Stp[4]+DB[Stp[5]];
MakeCon(Tmp,Adr);
If (Con[Adr[1,1],Adr[1,2],Adr[1,3]]=Nil)
Or(Con[Adr[2,1],Adr[2,2],Adr[2,3]]=Nil)
Or(Con[Adr[3,1],Adr[3,2],Adr[3,3]]=Nil)
Then YN:=False
Else Begin
Link[J]^.N1:=Adr[1,1];Link[J]^.N2:=Adr[1,2];Link[J]^.N3:=Adr[1,3];
End;{If Else}
End;{Else}
End;{While}
If YN Then Begin
For I:=1 To Theorem[N]^.ResN Do
Begin
Inc(Inf.Step);
Stp:=Theorem[N]^.Res[I]^;
Tmp:=DB[Stp[1]]+Stp[2]+DB[Stp[3]];
MakeCon(Tmp,Adr);
If Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Flag=2
Then Print(Tmp,True)
Else If Con[Adr[1,1],Adr[1,2],Adr[1,3]]=Nil
Then Begin
New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]);
Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Flag:=1;
Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Num:=J;
For L:=1 To J Do
Begin
New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Up[L]);
Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Up[L]^.N1:=Link[L]^.N1;
End;

12


End;{Else If Then}
Str(Adr[1,2],Stp);Ch:=Stp[1];
If Not(Def.Mark[Ch].Lab In Inf.MarkSet)
Then If (Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Flag=2)
And(Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Flag<>2)
Then Print(Tmp,True)
Else If Con[Adr[1,3],Adr[1,2],Adr[1,1]]=Nil
Then Begin
Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Num:=J;
For L:=1 To J Do
Begin
New(Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Up[L]);
Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Up[L]^:=Link[L]^;
End;
End;{Else If Then}
If Inf.Left=0 Then Begin Close(Fl);Halt; End;
End;{For I}
End;{End If}
End
Else ZuHe(Inf.ParamI[L1+1].Num,Theorem[N]^.ParamI[L1+1].Num,L1+1);
End;{Check}
Procedure ZHWork;
Procedure PLTry(Dep2:Byte);
Var I:Byte;
Begin
For I:=1 To M1 Do
If C[I] then
Begin
B[Dep2]:=A[I];
C[I]:=False;
If Dep2=M1 Then Check
Else PLTry(Dep2+1);
C[i]:=True;
End;
End;{ZHWork}
Begin
Fillchar(C,sizeof(C),True);
PLTry(1);
End;{ZHWork}
Procedure ZHTry(Dep1:Byte);
Var I:Byte;

13


Begin
If Theorem[N]^.ParamI[L1].Num>0
Then Begin
If Dep1<=M1
Then Begin
For I:=1 To N1 Do
If D[I] Then
Begin
A[Dep1]:=I;
D[I]:=False;
If Dep1=M1 Then ZHWork
Else ZHTry(Dep1+1);
D[I]:=True;
End
End
End
Else Begin
If L1<>3
Then ZuHe(Inf.ParamI[L1+1].Num,Theorem[N]^.ParamI[L1+1].Num,L1+1)
Else Check;
End;
End;{ZHTry}
Begin
FillChar(D,Sizeof(D),True);
ZHTry(1);
End;{ZuHe}

Begin
If (Theorem[N]^.Scope<=Inf.Scope)And
(Theorem[N]^.CondK<=Inf.CondK)And
(Theorem[N]^.CondN<=Inf.CondN)And
(Theorem[N]^.MarkI.Kind<=Inf.MarkI.Kind)
Then Begin
For I:=0 To 3 Do
If Inf.ParamI[I].Num<Theorem[N]^.ParamI[I].Num
Then Exit;
For Ch:='1' To '9' Do
If Inf.MarkI.MarkN[Ch]<Theorem[N]^.MarkI.MarkN[Ch]
Then Exit;
End
Else Exit;
For I:=0 To 3 Do
Begin

14


For J:=1 To Inf.ParamI[I].Num Do
Now1[I,J]:=Inf.ParamI[I].ParamCh[J];
For J:=1 To Theorem[N]^.ParamI[I].Num Do
Now2[I,J]:=Theorem[N]^.ParamI[I].ParamCh[J];
End;
ZuHe(Theorem[N]^.ParamI[0].Num,Inf.ParamI[0].Num,0);
End;

{===============================Procedure ReadIn==========================}
Procedure ReadIn;
Var F:Text;Tmp:Char;
Tmps:String[5];
Adr:TConData;
Tmp1,Tmp2,TmpN,i,j:Byte;
Begin
Write('请输入已知条件和需证结论的存储路径及条件名：');
Readln(Fn.Inn);
Write('请输入保存证明结果的存储路径及条件名：');
Readln(Fn.Outn);
Write('是否使用自建知识库（Y/N） '); ：
Readln(Tmp);
Write('多少步未得出结果就停止：');
Readln(Inf.StepN);
If (Tmp='Y')Or(Tmp='y') Then Fn.Flag:=True
Else Fn.Flag:=False;
If Fn.Flag=True Then
Begin
Write('请输入自建知识库的存储路径及条件名：');
Readln(Fn.Datan);
End;
Assign(F,Fn.Inn);Reset(F); //初始化输入文件
Assign(Fl,Fn.Outn);Rewrite(Fl);//初始化输出文件
With Inf Do
Begin
For Tmp:='1' To '9' Do MarkI.MarkN[Tmp]:=0;
Readln(F,CondK,CondN,ResN,MarkI.Kind,Scope);//读完第 1 行信息
Left:=ResN;
For I:=1 to CondK Do
Begin
Read(F,Tmp1,Tmp2);Read(F,Tmp);
ParamI[Tmp1].Num:=Tmp2;
Readln(F,ParamI[Tmp1].ParamCh);//读完第 2 行信息
For J:=1 to ParamI[Tmp1].Num Do

15


Begin
Used[ParamI[Tmp1].ParamCh[j]].Flag:=True;
Used[ParamI[Tmp1].ParamCh[j]].Kind:=Tmp1;
End;{For J}
End;{For I}
For I:=1 to CondN Do
Begin
Tmps:='';Read(F,Tmp);
While Tmp<>'.' Do
Begin
Tmps:=Tmps+Tmp;
Read(F,Tmp);
End;{While}
If Length(Tmps)=3
Then Begin
MakeCon(Tmps,Adr);
Str(Adr[1,2],Tmps);Tmp:=Tmps[1];
If Not(Def.Mark[Tmp].Lab In MarkSet)
Then Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Flag:=1;
Inc(MarkI.MarkN[Tmps[2]]);//累加某个运算符号出现的次数
End{Then}
Else Begin
Inc(MarkI.MarkN[Tmps[2]]);
Inc(MarkI.MarkN[Def.Mark[Tmp].Lab]);
End;{Else}
End;{For I}//读完第 2+N 行信息
Readln(F);
For I:=1 to ResN Do
Begin
While Tmp<>'.' Do
Begin
Tmps:=Tmps+Tmp;
Read(F,Tmp);
End;

16


If Length(Tmps)=3
Then Begin
MakeCon(Tmps,Adr);
End{Then}
Else Begin
End;
End;{With Inf}
Close(F);
End;

{=============================Procedure ReadData==========================}
Procedure ReadData;
Var F:Text;Tmp:Char;Tmps:String[5];
Tmp1,Tmp2,i,j,k,N5:Byte;
Adr:TConData;
Begin
Assign(F,Fn.Datan);Reset(F);K:=0;
While (Not Eof(F)) Do
Begin
Inc(K);
New(Theorem[K]);
For I:=0 To 3 Do
Theorem[K]^.ParamI[I].Num:=0;
With Theorem[K]^ Do
Begin
For Tmp:='1' To '9' Do MarkI.MarkN[Tmp]:=0;
Readln(F,CondK,CondN,ResN,MarkI.Kind,Scope);//读完第 1 行信息
For I:=1 to CondK Do
Begin
Read(F,Tmp1,Tmp2);Read(F,Tmp);
ParamI[Tmp1].Num:=Tmp2;
Readln(F,ParamI[Tmp1].ParamCh);//读完第 2 行信息
End;{For I}
For I:=1 to CondN Do

17


Begin
New(Cond[I]);
While Tmp<>'.' Do
Begin
Tmps:=Tmps+Tmp;
Read(F,Tmp);
End;{While}
Cond[I]^:=Tmps;
If Length(Tmps)=3
Then Inc(MarkI.MarkN[Tmps[2]])
Else Begin
MakeCon(Tmps,Adr);
Inc(MarkI.MarkN['^']);
End;
End;{For I}
Readln(F);//读完第 2+N 行信息
For I:=1 to ResN Do
Begin
New(Res[I]);
While Tmp<>'.' Do
Begin
Tmps:=Tmps+Tmp;
Read(F,Tmp);
End;
Res[I]^:=Tmps;
Readln(F);
End;{With}
Readln(F);
End;{While}
Inf.ThN:=K;
Close(F);
End;

{==============================Procedure Prove==============================}
Procedure Prove;
Var I:Byte;

18


Begin
While (Inf.Step<=Inf.StepN)And(Inf.Left>0) Do
For I:=1 To Inf.ThN Do
CheckWork(I);
If Inf.Step>=Inf.StepN Then Print('',False);
End;

{=====================================Main==================================}
Begin
Init;
ReadIn;
ReadData;
Prove;
Close(Fl);
End.

19

对简易几何机械化证明的进一步研究

Recommended

Recommended

More Related Content

Viewers also liked

Viewers also liked (17)

More from Lixun Peng

More from Lixun Peng (20)

Recently uploaded

Recently uploaded (14)

对简易几何机械化证明的进一步研究