谈以演化计算思想做机器证明与推理的构想[2]
演化证明与推理的操作举例与演化类型的初步划分
利其器，自然是为了善其事。现在我们接近了核心的问题，即如何将演化计算的思想应用于机器证明与推理中。
我们看几个证明序列的例子，会有很好的启示。
例子1 设α，β是Kφ中公式，证明：├（α→β）→（α→α） 。
证明
（1）α →（ β→α） （K1）
（2） （α →（ β→α））→（（α → β）→（α→α）） （K2）
（3） （α→β）→（α→α） （M）（1）（2）
这个证明过程是非常简单的，公理（K1）与（K2）等应该是我们的演化证明与推理系统初始化后所具备的，它们结合一定的形式规则就可以证明我们需要的结论。一般的，我们取两个不同家族的公式树进行演化，就有望得到目标公式树，这样的演化过程，我们称之为家族间演化。
例子2 设α是Kφ中公式，证明：├α→α 。
证明
（1）α →（（ β→α）→α） （K1）
（2） （α →（（ β→α）→α））→（（α →（ β→α））→（α→α））
（K2）
（3） （α →（ β→α））→（α→α） （M）（1）（2）
（4）α →（ β→α） （K1）
（5）α→α （M）（3）（4）
这个证明过程中略微有些复杂，整个证明的过程是由（1）中公式展开的。如何寻到（1）中公式，是证明的关键。传统的方法，很难意识到（1），但在我们的演化证明与推理中，寻到（1）是十分自然的，因为（1）中公式与（4）中公式是同家族的，我们只需把（4）对应的公式树的β结点换为β→α结点即可，注意到该公式树的标志集并没有改变，这样的演化过程，我们称之为家族内演化。
所以，若是由演化证明与推理来证明这个命题，成功的轨迹将是这样的：
（1） 对家族（K1）进行家族内演化；
（2） 依据（1）对家族（K2）进行家族内演化；
（3） 由（1）和（2）进行家族间演化；
（4） 引入家族（K1）的公式树；
（5） 由（3）和（4）进行家族间演化，成功。
可以看出，对于演化过程与策略的设计，将是复杂而关键的，这是我们将来的工作重点之一。
例子3 设α，β是Kφ中公式，证明： Ø（α→β）├ Øβ。
分析
这个命题的证明相当复杂，我们简略给出分析过程。
考虑到已知公式树中含α→β子树，我们有如下家族内演化结果：
（1）β→（α→β） （K1）
对于Ø的处理，我们是有倾向性的。将来详细设计有关演化的倾向性，也是我们工作的重点之一。如果我们知道如下内定理：
（2） （α → β）→Ø Ø（α→β）
（3） Ø Ø β → β
则我们进行家族间演化，可以得到：
（4）Ø Ø β → Ø Ø（α→β） （Tr）（1）（2）（3）
引入：
（5）（Ø Ø β → Ø Ø（α→β））→（Ø（α→β）→Ø β） （K3）
则由家族间演化可以得到：
（6）Ø（α→β）→Ø β （M）（4）（5）
已知：
（7）Ø（α→β）
则我们成功证明了命题：
（8）Ø β （M）（6）（7）
这个过程给我们的启示是丰富的。
首先，内定理
├ Ø Øα→α和├α→Ø Øα，
是可以另行证明的，我们引入它们，表明我们的演化证明与推理系统要及时记录整理常用内定理，并在新的证明推理过程中使用。
其次，对于联结词，推理过程应该有丰富的倾向性，虽然演化是随机的，但我们给出一定的演化倾向后，收敛速度会大大提升。
最后，（6）和（7）的演化，是一种新的演化方式，因为它们的公式树都不属于任何家族，如此，我们称团体的公式树参与的演化为团体演化。而家族内演化和家族间演化，可以统称为家族演化。团体演化和家族演化是相互影响相互作用的，但一般来讲，前者比后者更灵活更复杂。设计这种相互作用和相互影响，将是我们未来工作的核心。
上面的内定理的引入，是在形式系统Kφ中，但在直觉主义逻辑中，公式
Ø Øα→α
并不是内定理。我们的演化证明与推理系统在软件设计过程中，要严格依据形式系统的内容进行开发。下面我们就考虑其它逻辑形态的例子，选取的是模态逻辑的一个简单例子。形式系统为系统K。
例子4 设α是K中公式，证明：□α↔ Ø ◇ Øα 。
证明
（1）α ↔ ØØα ThP15
（2）□α ↔ ØØ □α （1）×SB
（3）□α ↔ ØØ □ Ø Øα （2）（1）×RES
（4）□α↔ Ø ◇ Øα （3）（D◇）×RES
这个证明过程表明，我们上面的讨论的概念和原则在这里是有效的。演化证明与推理的方法，是一个基本的方法。
综上，演化证明与推理在形式化证明过程中是有很好的切入点的。基本上，其演化过程的类型可划分为：
这其中有大量的设计工作，在上述分析中曾提到一些，但在实际的演化计算和机器证明与推理相融合的过程中，肯定还有众多我们没有意识到的问题。所以，在理论上，与软件系统上，我们要作好协调。边进行理论革新，边接受实践的检验。
演化证明与推理的展望和软件开发方案大略
一直在想，机器何时方能通晓人事。大规模的科学运算与非数值数据的处理，计算机是能够做到了。可是，知人事之微妙，似乎永远是机器的禁区。人工智能发展缓慢；人类的计算能力，计算机已经超过了，可是人类的联想、创新能力，计算机却没有学到。
如果计算机的演化证明与推理是可行的，希望能于此有所突破。演化计算的思想是不拘一格，拥有开阔的视野和自组织、自优化能力，这都能补充传统机器证明与推理方法的不足。如此，我们看下图：
图中，1为基于形式系统的演化证明与推理模型，2为泛型演化证明与推理模型，3为演化证明与推理的语义模型，5为人类活动的识别与理解模型，4为未知的过渡模型。
下面简单叙述这个系统，如上所述，它由5个模型有机搭配共同组成，试图帮助计算机辨识人事。
基于形式系统的演化证明与推理模型，就是本篇文章所重点讨论的模型，也是我们工作的入手点。
形式系统固然可以有丰富的语义解释，但形式系统并不能囊括人类所有的知识、思想，所以我们渴望能寻到一个新的模型，也基于演化计算的思想，来模拟人类的更广阔的思维活动。我们暂称之为泛型演化证明与推理模型。
1遵循“严格形式化原则”，但对于2，我们说，遵循另外一种原则，我们称之为“模糊不违背环境原则”。比如，在基于形式系统的演化证明与推理模型的不同演化过程中，尤其是团体演化过程中，会产生大量的公式树，如果不合于我们的目标，我们会丢弃；但在泛型演化证明与推理模型中，只要切合一定的环境因素，我们就把命题保留。二者方向不同，但相反相成，它们在5个模型中结合的最紧密，是我们系统的内核部分。
演化证明与推理的语义模型是内核的语义实现部分。
人类活动的识别与理解模型，是人工智能的各类分支学科的模型，比如自然语言理解与处理模型，计算机视觉理解与处理模型等。该模型不直接和演化证明与推理的语义模型相联系是有原因的。因为这项事业是如此之艰难，各模型的建立完善工作是各自为战的。比如自然语言理解与处理，我看过的最好的模型，是中科院黄曾阳先生的HNC理论。既然是各自为战，HNC理论的模型是相对独立的，我们还无法考虑到相互的需求，那样的话复杂度也太大了。所以，将来我们需要一个未知的过渡模型，来完成它们与系统内部的连接转化工作。
这也就是我们的4（过渡模型）存在的要义。
当有一天我们走向了统一，也就是图5的系统比较完善的时候，我们的计算机将具有人类的特点。人工智能，就算确实的前进了一大步。
这项工作是有意义的，但也是艰难的。我们将由1（基于形式系统的演化证明与推理模型）入手，做塌实的理论革新与实践检验工作。这个过程也将是反复的，而这个过程中我们的软件有如下几个阶段需要做评审工作：
（1） 系统的基本建立与部分公式的证明；
（2） 演化过程的优化与系统的扩展；
（3） 基于形式系统的演化证明与推理模型基本完成。
毫无疑问，我们会一如既往的做下去。可以看出，目前我们认为这个方案是有效的；但我们希望能通过实践证明，演化证明与推理是有效的，亦或无效的。
<2003-9-25 初记于武汉>
参考资料：
（1）周北海 著 ，《模态逻辑》，中国社会科学出版社，1996年。
<完>
------------------------------------------
声明：本文作者保留所有权利,您若有任何建议请送至percylee@126.com
