需要说明的是，图中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）。
<未完>
------------------------------------------
声明：本文作者保留所有权利
本类阅读TOP10
