限定逻辑的表列方法，本文主要内容关键词为：逻辑论文,方法论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B81 文献标识码：A 文章编号：1674－8425(2013)09－0027－05
doi:10.3969/j.issn.1674－8425(s).2013.09.005
限定逻辑由McCarthy(1980)[1]创立，随即引起了很多逻辑学家的重视和研究，迅速发展成为包含个体域限定、谓词限定、公式限定等多种不同限定逻辑的内容丰富的非单调逻辑的一个重要分支。限定逻辑与其他非单调逻辑一样，目前仍然存在一些争议和有待解决的问题。限定逻辑最大的困难在于其算法的设计，即在给定的限定之下，如何确定某个句子是否可被推出？针对这个问题，本文介绍命题限定逻辑和公式限定逻辑的两种表列算法。
一、从谓词限定到公式限定
与缺省逻辑、非单调模态逻辑不同，限定逻辑并不引入新的语言表达手段，而是直接在标准逻辑的语言中将常识句形式化进而用经典逻辑的推演刻画非单调推理。McCarthy(1986)[2]借助于一个特殊的谓词Ab(abnormal)来表示常识句。以“鸟会飞”为例，“鸟会飞”可以形式地表示为：
x(Bird(x)∧
Ab(x)→Fly(x))。意思是，如果一只鸟不是反常的，那么它会飞。如果我们现在知道：
那么，怎样才能从(1)和(2)得出Fly(Tweey)的结论？McCarthy(1986)[2]提出的方案是限定谓词Ab，对谓词Ab的限定就是极小化它的外延。对一元谓词P来说，如果a是P的外延中的一个对象，则称a满足P或者a是P的一个实例。当前主体已知的信息用一组句子表示，一个有穷的句子集称为一个理论，其中的每个句子称为“公理”。用T表示一个理论，相对于T极小化谓词P的外延(P出现于T的某个句子中)，直观上说就是断定，就T所提供的信息而言，已知满足P的所有个体就是P全部的实例。P的极小是相对于T的，意味着如果再减少P的外延就会导致与T不一致。上面(1)和(2)提供的信息并没有明确说明有某个个体是反常的鸟，因此，相对于(1)和(2)，Ab的外延极小化为一个空集，于是得到结论：x(Bird(x)→Fly(x))和Fly(Tweety)。这就是谓词限定逻辑的基本思想。为了从语形方面实现这一思想，McCarthy(1986)[2]给出了谓词限定的定义。
首先约定一些记法。
定义3(极小后承) A是T的P-极小后承，当且仅当A在所有T的P-极小模型上为真。
一个一致的理论可能有一个或多个极小模型，也可能没有极小模型。对于一阶逻辑句子集的某些类型的子集来说，极小模型总是存在的，例如只包含全称公式的全称理论等。因此，关于限定逻辑的研究往往限定在一阶逻辑的某个(通常是可判定的)子集上。如果一个理论T的每一个模型都有一个P-子模型M，使得M是T的P-极小模型，则称T是相对于P的良建理论。研究表明，谓词限定逻辑相对于良建理论的表达能力不够强。例如：T=｛x(Bird(x)∧Ab(x)→Fly(x))，x(Penguin(x)→Bird(x)∧Fly(x))，Bird(Tweey)｝，T是一个良建理论，在T中限定谓词Ab后，并不能得出我们想要的结论Fly(Tweey)，因为在T中限定Ab并不能反映Ah与Fly这两个谓词之间的关系，存在T的极小模型使得Fly(Tweety)在其中为假。由于谓词限定存在这样一些问题，McCarthy(1986)[2]提出了更为一般的公式限定逻辑，在限定T中的一组谓词的同时，允许其他谓词的外延发生相应的变化，这种限定也称为平行限定(Parallel Circumscription)。
限定逻辑及其极小后承语义最初是在一阶逻辑层面上提出来的，这套方法同样适用于命题限定及命题层面的极小后承语义。在命题逻辑中，被极小化的是一集原子公式。令V和V′是命题逻辑的两个赋值，V≤V′当且仅当，对于所有的命题变元p，如果V(p)=1则V′(p)=1。一个一致的命题集总有其极小模型。将命题层面的极小后承关系记为
，
当且仅当A在所有T的极小模型上为真。
一个逻辑的表列方法必须以其成熟的语义理论为基础。由于一阶限定逻辑有极小模型的存在性、个体的唯一命名等问题，为一阶限定逻辑设计一种表列算法是非常困难的。Olivetti(1992)[3]给出的命题逻辑极小后承的表列建立了一种寻找极小模型的方法，对于一阶限定逻辑的表列设计具有很强的启发性，因此首先介绍命题限定逻辑的表列演算。
二、命题限定逻辑表列
与公式限定类似，一般的命题限定也包括三类原子公式：一类是被极小化的，记为
；一类是可变的，记为
；其他原子公式是固定不变的。首先考虑所有原子公式都被极小化这种基本情况。Olivetti(1992)[3]给出的表列展示了非单调逻辑表列不同于标准逻辑表列的一些特殊方法。
根据前面的定义，对于Γ的两个模型
和
，
当且仅当对于任一命题变元p，
，即，在下取真的命题变元的集合是在下取真的命题变元的集合的子集。因此，要判断一个Γ-模型是否极小，只需考虑表列中那些来源于Γ的(原子)公式的情况，因为Γ-模型仅由来源于Γ的公式描述，与来源于A的公式无关。为方便表述，以下称Γ为前提，A为结论。Olivetti首先对标准命题逻辑的表列规则作了改修，利用标号t和f将前提Γ和结论A中的公式区别开来。表1给出了α和β-公式及其表列公式。
Olivetti表列规则的特征是，所有规则结论中的公式的标号都与前提公式标号相同，所以，在初始结点标有(tΓ，fA)的表列中，所有来源于前提Γ的公式都标示“t”，称之为t-公式；所有来源于结论的公式都标示“f”，称之为f-公式。表列中的“封闭”概念相应地修改为：如果一个枝B上同时出现tA和tA、或者同时出现fA和fA、或者同时出现tA和fA，那么枝B是封闭的。如果一个表列所有的枝都是封闭的，则表列是封闭的。
将命题变元及其否定式统称为“字符公式”。如果枝B上的所有的t-公式都是字符公式，则B是t-完成的；如果枝B上的所有的f-公式都是字符公式，则B是f-完成的。
表列的构造程序为：
步骤1 将(tΓ，fA)置于初始结点上。
步骤2 如果枝B上有一个α公式，则从B上删除α，然后在B的末端增加
；如果枝B上有一个β公式，则从B上删除β，然后在B的末端增加两个分枝并分别在其末端增加
。
步骤3 检查任一枝B，如果B是t-完成的且是f-完成的，则B的扩充结束。如果表列上所有的枝都或者扩充结束或者封闭，则表列是完成的。程序结束。否则返回步骤2。
定义At(B)是B上所有标t的命题变元的集合：At(B)=｛p∶tp∈B｝。下面给出的是可忽略的枝(对应非极小Γ-模型)的两个条件。
一个开放的枝B是可忽略的，如果：
(1)B是完成的，并且存在字符公式p，使得fp∈B而tp
B。或者
(2)存在另一个完成了的枝B′，使得At(B′)
At(B)。
条件(1)不像条件(2)那样显然，我们对(1)略作解释。设想对fp中的子公式p使用切割规则得到：
则右边的分枝封闭。而如果左边的分枝
是一个潜在的Γ-模型，那么总存在另一个Γ-模型比少一个命题变元p，因此表示的Γ-模型一定不是极小的。
如果一个表列的所有枝或者是封闭的，或者是可忽略的，则称该表列是mp-封闭的。一个关于(tΓ，fA)的mp-封闭的表列是对
的一个表列证明。
这种方法可以推广到带一组可变原子公式的一般命题限定(Kuhna,1992)[4]。
三、公式限定逻辑的子句表列
文献[3]和[4]中的表列都需要将一个枝B与其他完成的枝加以比较才能确定B是否对应一个极小模型，而一阶逻辑的表列可能出现不终止的无穷长的枝，基于完成的枝的极小模型判断方法无法直接推广到一阶逻辑。在一阶逻辑表列中，存在量词规则引入的个体常元一般被假定指称不同的个体，而当谓词或个体域被极小化时，不同的个体常元能否指称同一个体直接关系表列证明的可靠性，这被称为唯一命名设定问题。此外，并不是任何一个一致的一阶公式集都有其极小模型。由于存在这样一些问题，似乎无法直接将命题限定表列推广到一阶语境，也无法期待一种有效率而完全的一阶限定的表列证明程序。Niemala(1996)[5]提出的一阶公式限定表列是将一阶公式限定于子句形式、将语义解释限定于Herbrand-模型的一种表列证明方法。
Niemela给出的限定推理的表列是不加标表列，有2条表列扩充规则：
Niemela证明了该表列演算相对于上述语义是可靠的、完全的。
表列方法本身是单调性的，如果∑
A，那么存在关于｛∑，A｝的封闭的表列，此时对于任一公式集Γ，关于｛∑，Γ，A｝的表列也是封闭的。借助于某些方法，单调性的表列方法可以运用于非单调推理。限定逻辑表列依赖于某些外部条件，根据事先规定的枝的选择条件排除某些开放的枝，从而得到比标准逻辑表列更宽松的“封闭”条件，刻画了比标准逻辑推演更强的非单调推演关系。
收稿日期：2013－06－25