需要说明的是,图中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)。
<未完>
------------------------------------------
声明:本文作者保留所有权利