谈以演化计算思想做机器证明与推理的构想
-----------说演化证明与推理的可能性
作者：李连华（percylee@126.com）
摘要：本文详细讨论由演化计算思想来做机器证明与推理工作的可能性，提出了演化证明与推理的相关概念和初步框架，并由此对演化证明与推理作出了展望。
关键字：机器证明与推理，演化计算，演化证明与推理，人工智能
证明与推理，是智能的高级表现形式；而机器证明与推理，则为人工智能的核心领域之一。近年来国内在机器证明的几何定理证明的道路上，取得了骄人的成绩，尤其是吴文俊先生与他的“吴方法”，开创了几何定理证明乃至机器证明的新局面，而展开了其“数学机械化”的梦想。
演化计算，作为一种新兴的计算模型，其成功已足以成为智能计算的基础。作为基于随机搜索策略的自组织、自适应系统，演化计算具有广泛的适应性。
大概从几个月前，根据自己在演化计算方面的经验，与一点点的机器证明知识，我开始思考这个问题：是否可以依据演化计算的思想，来做机器证明与推理的工作？这样，我们可以给之一个新的定义，不妨称为演化证明与推理。
我目前还没有关于“吴方法”的详细的资料，只能找到简短的描述，不足以有所借鉴。所以以下的讨论，自然不是由几何定理的机器证明展开，而是从形式系统出发。
当然，从形式系统出发，证明与推理过程是严格基于逻辑推理的公理与形式规则的，而演化计算的基本策略是随机策略，又如何将它们融合在一起，让演化计算很好的为机器证明与推理服务呢？换句话，这种思路是不是可能且有效的？下面我从初步的思路出发，主要谈这个问题，并在这个过程中，给出一些新的定义，试图展示演化证明与推理的初步框架。
数据表达形式
形式系统的建立，是基于形式语言的。用演化计算的思想，来做机器证明与推理，首先的问题是：
如何找到一种数据表达形式，即可以完全表达形式语言与形式系统，又可以方便的进行演化计算的编码？
如果说演化证明与推理如新生的微芽，那么这个问题，就是种子的第一层外壳。不给出一个很好的答案，有很多思想的冲动，但却不知如何表达了。
形式语言，我们以一阶语言φ为例，当然，我们可以加入模态算子 □ 和 ◇，但目前来讲还是没有太大必要。在讨论人类具体的证明过程给我们的启示时，我们再引入模态逻辑的证明序列。
一阶语言φ，主要构成部分为：
1， 非逻辑符号
（1） 个体常元，如c；
（2） 谓词变元，如F；
（3） 函数变元，如f；
2， 逻辑符号
（1） 个体变元，如x；
（2） 量词符号（作用域符号），如" 与 $；
（3） 联结词符号，如Ø，∧，∨，→，↔等；
（4） 辅助符号，如‘（’，‘，’，‘）’等。
在此基础上，有项和公式的定义，我们不再赘述。只举两个公式的例子如下：
公式1：α →（ β→α） ；
公式2： "x（α→β）→（"xα→"x β） ；
显然对于一阶谓词逻辑演算的形式系统Kφ，它们分别是公理（K1）和（K6）。这些逻辑公式表义是非常丰富的。不考虑其它，我们先问，用什么形式，作为我们数据表达的形式？对于数学讨论，使用“串”是非常好的。但对于我们的讨论，却并非如此，算法设计就过于复杂，有很多问题要面对。比如公式（1）是一个公理，但它的形式不是唯一的，亦等价于下面的公式：
公式3：α →（（β→γ）→α） ；
但若要机器明白这一点，对于使用串的算法，即使可以做出来，也是相当复杂的。更不用说更为复杂的公式形式了。
有一个比较自然的表达形式，就是采用“树”，公式(1)和公式(3)的树形结构为：
这样，似乎很方便（我们后边再谈），而且，对于演化计算的编码来讲，也是非常容易的。但是，问题很快又来了，公式（2）如何表达？这种限定域的信息，如何方便的表达出来，而兼顾演化计算的编码效率？
这个问题，前后困扰了我一个多月，曾想改造树形结构，后又想用广义表，后又回来改造树形结构。
初步的，我们给出如下的表达系统：
需要说明的是，图中p是一个指针，可指向（3）的接点或为空，而（3）中的string_val，可以是如下面的字符串：
"x1 "x2 $y 。
对于谓词变元与联结词的处理基本上是相同的，只是后者指向子树的指针的个数是一定的；而对于个体常元与个体变元的处理也是相同的。由此，我们可以表达公式（2）如下：
其中，三个限定域接点内容分别为：
string_val1: "x ;
string_val2: "x ;
string_val3: "x 。
且，α与β都是公式，实质上都是子树，所以它们表示为一个带p指针的结点。
使用这个表达方式，我们可以基本上解决形式系统的表示问题，如果要改变（扩充）形式系统的逻辑形式，比如我们要讨论模态逻辑，则模态算子可以视作一元的逻辑算子，表示类似于Ø。
我们下面的讨论，都是基于这种数据的表达方式。
演化证明与推理的相关定义
为了便于做进一步的讨论，我们需要解决如下的问题：
形式系统的公理与形式规则，实际上都代表了一类公式，这我们应如何处理？公式之间一定的关系如何表达？
比如，对于公理（K1），在图1中就展示了它的两个结论（注意我们可以视这样的树形式为我们图2的表达方式的简略形式）。如何判定它们是“相同”的呢？
我们给出如下的定义。
公式树T 基于图2的表达方式，所给出的形式系统的公式，称为公式树，记为T。图3是一个公式树的标准形式，图1则看作相应的简略形式。
公式树的标志集K 若公式树为形式系统相应的公理、形式规则或内定理，则有唯一的等式集描述树中的一些结点关系，它表现了该公理、形式规则或内定理的内涵本质，我们称之为该公式树的标志集，记为K。比如，对于公理（K1），图1中有两个不同的公式树，树的根结点为root，其左孩子为root->leftChild，右孩子为root->rightChild，则该公式树的标志集为：
{ root=→, root->rightChild=→, root->leftChild = root->rightChild->rightChild }。
家族H 形式系统的任意一个公理、形式规则或内定理，它的所有公式树都在同一个家族里，则这样的家族相应于其公理、形式规则或内定理是一一对应的，家族的标志为该公式树的标志集，家族记为H。
团体O 公式树的一个集合，如果不是一个家族，我们称之为一个团体，记为O。
同家族关系～ 若两个公式树T1和T2在同一家族H里，则T1和T2具有“同家族关系”，记为～，后可加小括号说明家族名称，即：
T1～T2 （H） 等价于 T1 ∈ H且T2 ∈ H。
这样，根据这些概念，我们可以写算法判定图1中的两个公式树是“相同”的，即在同一家族，若公式（1）对应为公式树T1，公式（2）对应为公式树T2，公理（K1）对应为家族H1，则：
T1 ～ T2 （H1）。
<未完>
------------------------------------------
声明：本文作者保留所有权利
