P.Linux Laboratory

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