摘要：“机械化证明”，就是用计算机进行判断、推理、证明等活动的集合。做这个课题的关键，就在于如何利用计算机模拟出人脑的推理过程。我采用的思维方式，

即：归纳->演绎->推理 的思维过程。所以，整个搜索系统由以下三大部分组成：

      1.知识库  ：包括当前证明所需的全部公式定理。

      2.扩展规则：控制节点扩展的方案。作用于当前一个节点，产生其后继节点。

      3.控制策略：控制节点中信息与知识库之间的对比，测试是否已证到需证结论或得出无法证明。

    然后建立一个Con函数，用信息的Def值为参数，生成Con地址，填入Con表中，在搜

索对比时只要查询Con表的地址，就可以知道是否有相同信息，大大加快搜索效率。（Con函数，Con表, Con地址，Def值的含义见论文）

关键更新：Con表存储结构。

“人工智能学”就是智能机器所执行的通常与人类智能有关的功能，如判断、推理、证明、识别、感知、理解、设计、思考、规划、学习和问题求解等思维活动。实现人工智能，有两种方法，一是在硬件上，一是在软件上。用硬件方法就是做出仿生物处理器，让处理器的运行模拟人脑的运行模式，但是就目前的现实来看，生物处理器在短时间内不可能被制造出来。所以就目前而言，我们只能靠软件的方法，也就是用程序来模拟人脑的思维方式，来实现人工智能。

清华大学吴文俊教授曾经成功的完成过一个机械化证明程序，提出了“吴氏算法”，可以证明欧拉几何、平面几何等问题，但是吴文俊教授的设计思想比较复杂复杂，主要从数学方面入手，而不是从人脑的思维方式入手，所以需要很深的数学知识才能理解。此外还有面积法，坐标法等机械化证明方法，但这些算法也和吴文俊教授差不多，都不是主要从人脑的思维方式入手，偏向数学方法，不是大部分人可以理解的。

做这个课题的关键，也是难点之处，就在于如何利用计算机模拟出人脑的推理过程。

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

而人们进行证明，当然也是这个思维过程。人们首先根据以往归纳的经验（包括题型的固定解题思路，公式定理等）确定此问题的类型，判断大致思路，然后根据题目的实际条件在一定范围内进行演绎，修改硬套的解题思路，摸索符合实际情况的解题方法，同时搜索大脑里的对定理公式的记忆，调用其中相关的（即有可能使用到的）公式定理，与本问题已知条件进行对比，然后推理出本题的解题思路，得出证明步骤或一些结论结论。

根据这些简单的分析，大致模拟上面分析的过程，就可以初步建立起证明程序的计算机算法模型。

于是，一开始我很自然地想到用“广度优先搜索”和“深度优先搜索”，以及“双向搜索”等搜索方法为核心，佐以合理的数据结构，加以一定的剪枝优化来编写程序。

为了能够让计算机“明白”要用到的公式定理，首先必须建立一个完备的知识库，知识库中包含了证明所需的“知识”——计算机能够识别的按一定格式储存的公式定理数据库。然后，在搜索的时候，需要根据搜索知识库的情况，扩展一些条件节点。所以必须有一个扩展规则来作用于一个节点，产生其后继节点使搜索能够进行下去。此外，还需要一个控制策略，来控制搜索的过程和方案，以及测试是否达到终止条件（包括达到需证结论、得出无法证明或满足用户自定义的终止条件），记录扩展信息等。

所以，整个搜索系统由以下三大部分组成：

  1.知识库  ：包括当前证明所需的全部公式定理。可以在程序中内置完整的知识库，也可以通过数据库的形式从程序外部提供。

  2.扩展规则：控制节点扩展的方案。作用于当前一个节点，产生其后继节点。

  3.控制策略：控制节点中信息与知识库之间的对比，测试是否已证到需证结论或得出无法证明或满足用户自定义的终止条件，记录节点扩展时产生的信息。

由于进行搜索时，必须要有统一的数据记录形式，才能完成搜索，而用户输入的条件不一定按照程序定义的数据结构来输入，因为为了方便处理，程序使用的数据结构都比较复杂，所以还应该建立一个格式化系统，来对用户输入的一般格式的条件、知识库等进行格式化处理，储存为程序运算储存使用的格式。

根据这些组成部分及其作用，我提出了如下的算法框架（包括算法说明图）：

{   
    1.读入已知条件及需证结论。
    2.判断用户是否提供知识库。
    3.1.如果用户提供数据库，格式化已知条件、需证结论以及用户提供的外部数据库；
    3.2.如果用户不提供数据库，格式化已知条件、需证结论，初始化程序内置知识库或外部自带的数据库。
    4.按控制策略开始搜索知识库，对比已知条件。
    5.按扩展规则扩展当前节点。
    6.按控制策略判断是否满足终止条件。
    7.1.如果满足终止条件则输出结果，结束程序；
    7.2.如果不满足终止条件则转(4)继续搜索。
}

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

有了上面定义的编号（Def值），计算机就可以在处理数据时，通过扫描编号来判断或得知数据的类型，从而缩小题目中考虑的范围，例如是否考虑空间几何，有关于没有垂直、平行的条件或须证结论等等。这样可以只搜索知识库中可能用到的公式定理，例如题目不考虑空间几何则根本不需要搜索立体几何数据库。这样可以减少大量无谓的搜索，在很大程度上提高搜索的效率。否则，在不知道数据类型的情况下进行盲目搜索，且不说其产生大量垃圾节点降低搜索效率的坏处，单立体几何与平面几何就有不少条件相同但结论不同的定理，例如ab、bc，在平面几何里可以推出a//c的结论，但是立体几何中a、c可能异面垂直可能平行还可能就是异面直线，这是完全不同的结论。因此，用编号来描述数据类型不仅可以提高搜索效率，还可以避免错解的发生。

接着，为了方便对搜索时的信息进行处理，必须建立合理的数据结构。

所谓合理地数据结构，首先，要能准确无误的表达出问题描述的信息、每一步搜索的具体情况；然后，要能够使程序方便地得知目前证明中全局进行的状况，；最后，还要顾及数据所占用的空间，把空间占用控制在大部分主流计算机比较容易承受的范围之内。

经过思考和尝试，我首先确定了如下的输入文件（包括已知条件和需证结论，知识库）的数据结构，用户可以按这个结构输入题目的信息和自建知识库。

{  输入信息数据结构：

   已知条件和需证结论标准格式：
   [  
      第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’]OfString这样的数据结构就可来储存哪些标识符可用及已用的标识符代替的是什么。比如当’A’标识符还未使用时，Ch[‘A’]=’’；当’A’标识符代表题中的AB时，则Ch[‘A’]=’AB’。

然后就必须考虑如何来建立中间节点的数据结构和储存方式、以及与知识库对比的方式。如果采取直接记录法，即用字符串形式直接记录下定理公式，保存在节点里。这种储存方式虽然直接明了，但是与知识库或逆向节点对比时就只能采用把节点里的条件全排列组合，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，ab和cb在平面几何也可以推出a//c，但只要满足a//b、b//c或在平面几何中ab、cb两个中的一个，就可以推出a//c，而不需要两套都满足。

由于证明的这个特殊性，从正向搜索和从逆向搜索的扩展策略就有一定的区别。顺序证明由于用过的条件可以和新推出的结论一起使用推出新的结论，所以计算机正向搜索的扩展策略可以只在原节点基础上不断添加信息即可。而从结论反推，可能有几条思路都可以到达结论。所以，逆向搜索的扩展策略是每次反推出的结论的充分条件都要用一个新节点来保存。因此控制策略中只要某时刻搜索中逆向搜索出的某一节点中的信息在正向搜索的节点中都能找到，即满足了一个终止条件则认为证明成功。

于是，我决定建立一个固定大小带有Boolean变量域的表（Com=Array[起始值..终点值]  Of  Data）用来储存正向搜索的节点信息并作为对比表，称之为Con（Contrast比较）表，其地址称之为Con地址，初始化Boolean变量域为False。而逆向用数组指针来存储（即数组+指针，如Dat=Array[1..100] of  ^List）。这样，正向节点每一条信息就产生一个唯一的地址，把表中此地址的Boolean变量域的值赋为True，通过查一次表，就可以判断是否有相同信息。但是通过实践，逆向搜索很多时候反而会降低效率，因为逆向搜索节点数量不断膨胀，搜索次数增加，还不如只有正向搜索，于是我决定只采取正向搜索。

现在，关键问题到了如何使一条信息只生成一个唯一的地址。因为只有这样，对照时，同样的信息才能产生同样的地址，所以对比时只要此地址的Boolean域值为True则说明有相同的一条信息，如为False则说明没有相同的一条信息。

 如何使不同的信息生成唯一的地址，同时又能节省空间，节省时间，我尝试了不少方案。例如线性函数。但是都或多或少有些毛病。通过试验，综合时间效率和空间效率，我采用了一种最简单的方案：对于一个条件，我取其Def值，转化为字符串进行加运算，生成一个新字符串，把这个字符串转化为数字即为这条信息的Con地址。例如，"ab"这个条件，"a"的Def值为37，""的Def值为6，"b"的Def值为38，则生成的Con地址字符串为"37"+"6″+"38″="37638″，转化为整形数据37638即为"ab"这条信息的Con地址。由于同一个符号的两边的字符若相同，其生成的地址必然相同。但是"ab"和"ba"实际是等价的条件，但是它们的Con地址却一个是37638，一个是38637，这是两个不同的Con地址。

为了解决这个问题，我提出了两个方法，一是生成Con地址时可把另一个对应等价条件的Con地址赋为True，因为等价条件的Con地址是对称的，知道一个肯定可以推出另一个。二是生成Con地址时，把Def值小的放前面，比如"ab"生成的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个数据，空间效率提高更加明显。

还有一种特殊情况，就是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:Array[元素下界..元素上界，元素下界]Of对应关系”记录元素之间的关系。那么对于两重关系的元素，只要在[A,B]上赋值第一种关系，在[B,A]上赋值第二种关系即可，这样空间利用就达到了最大化。

在对比的过程中，还有许多的剪枝可以用到，这样可以减少无谓的搜索。比如：当某条定理的适用范围不包括我们要证的问题的考虑范围，则根本不需要去对比这条定理；当某条定理条件中的参数数量大于我们已用的参数数量时，不需要对比这条定理；当某条定理条件中的数学符号数量大于我们已用的数学符号数量时，不需要对比这条定理；当某条定理条件中的某种类型参数数量大于已知的这种类型参数数量时，不需要对比这条定理；如果把定理都搜索了一遍，没有任何结论可以推出，则这个结论不可能用已知的知识库证明出来，输出不可证……

此外知识库的对比时，数据库用的标识符很可能与题中的不一致，所以要将定理中的标识符与已用的标识符进行替换，再进行对比。假设目前对比的定理中，点参数有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;
    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;          //考虑范围和参数总数
    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域为假
          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;
           A[1,3]:=Def.Lable[St[3]];
          End
    Else Begin
           A[1,1]:=Def.Lable[St[1]];
           A[1,3]:=Def.Lable[St[3]];
           A[2,1]:=Def.Lable[St[5]];
           A[2,3]:=Def.Lable[St[1]];
           A[3,1]:=Def.Lable[St[5]];
           A[3,3]:=Def.Lable[St[3]];
           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;

{============================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
          Else Begin
            Inc(J);New(Link[J]);
            Link[J]^.N1:=Adr[1,1];
            Link[J]^.N2:=Adr[1,2];
            Link[J]^.N3:=Adr[1,3];
          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
            Inc(J);New(Link[J]);
            Link[J]^.N1:=Adr[1,1];Link[J]^.N2:=Adr[1,2];Link[J]^.N3:=Adr[1,3];
            Inc(J);New(Link[J]);
            Link[J]^.N1:=Adr[2,1];Link[J]^.N2:=Adr[2,2];Link[J]^.N3:=Adr[2,3];
            Inc(J);New(Link[J]);
            Link[J]^.N1:=Adr[3,1];Link[J]^.N2:=Adr[3,2];Link[J]^.N3:=Adr[3,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;
                 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
                         New(Con[Adr[1,3],Adr[1,2],Adr[1,1]]);
                         Con[Adr[1,3],Adr[1,2],Adr[1,1]]^.Flag:=1;
                         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;
  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
    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
    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);
       New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]);
       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
       New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]);
       New(Con[Adr[1,3],Adr[1,2],Adr[1,1]]);
       Inc(MarkI.MarkN[Tmps[2]]);
       New(Con[Adr[2,1],Adr[2,2],Adr[2,3]]);
       Str(Adr[2,2],Tmps);Tmp:=Tmps[1];
       Inc(MarkI.MarkN[Def.Mark[Tmp].Lab]);
       New(Con[Adr[3,1],Adr[3,2],Adr[3,3]]);
       Str(Adr[3,2],Tmps);Tmp:=Tmps[1];
       Inc(MarkI.MarkN[Def.Mark[Tmp].Lab]);
     End;{Else}
   End;{For I}//读完第2+N行信息
   Readln(F);
   For I:=1 to ResN Do
   Begin
    Tmps:=”;Read(F,Tmp);
    While Tmp<>’.’ Do
    Begin
      Tmps:=Tmps+Tmp;
      Read(F,Tmp);
    End;
    If Length(Tmps)=3
     Then Begin
       MakeCon(Tmps,Adr);
       New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]);
       Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Flag:=2;
     End{Then}
     Else Begin
       New(Con[Adr[1,1],Adr[1,2],Adr[1,3]]);
       Con[Adr[1,1],Adr[1,2],Adr[1,3]]^.Flag:=2;
       New(Con[Adr[2,1],Adr[2,2],Adr[2,3]]);
       Con[Adr[2,1],Adr[2,2],Adr[2,3]]^.Flag:=2;
       New(Con[Adr[3,1],Adr[3,2],Adr[3,3]]);
       Con[Adr[3,1],Adr[3,2],Adr[3,3]]^.Flag:=2;
     End;
   End;{For I}//读完第3+N行信息
  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
     Begin
      New(Cond[I]);
      Tmps:=”;Read(F,Tmp);
      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[‘^’]);
         Str(Adr[2,2],Tmps);Tmp:=Tmps[1];
         Inc(MarkI.MarkN[Def.Mark[Tmp].Lab]);
         Str(Adr[3,2],Tmps);Tmp:=Tmps[1];
         Inc(MarkI.MarkN[Def.Mark[Tmp].Lab]);
      End;
     End;{For I}
     Readln(F);//读完第2+N行信息
     For I:=1 to ResN Do
     Begin
      New(Res[I]);
      Tmps:=”;Read(F,Tmp);
      While Tmp<>’.’ Do
      Begin
        Tmps:=Tmps+Tmp;
        Read(F,Tmp);
      End;
      Res[I]^:=Tmps;
     End;{For I}//读完第3+N行信息
    Readln(F);
   End;{With}
   Readln(F);
  End;{While}
  Inf.ThN:=K;
  Close(F);
End;

{==============================Procedure Prove==============================}
Procedure Prove;
Var I:Byte;
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.