软件学报  2017, Vol. 28 Issue (7): 1759-1772   PDF    
贪婪缺省逻辑
陈博1,2, 曹存根1, 眭跃飞1    
1. 中国科学院 计算技术研究所 智能信息处理重点实验室, 北京 100190;
2. 国网山东省电力公司 电力科学研究院, 山东 济南 250001
摘要: 提出了一种贪婪缺省逻辑,旨在构造扩展的过程中尽可能地保留缺省规则当中的信息.给出了贪婪缺省逻辑的推演系统——GD系统和贪婪缺省的GD-扩展的定义.并且证明了对于缺省理论(T,Δ)的一个扩展,必定存在一个贪婪缺省理论的GD-扩展,使得缺省逻辑的扩展是贪婪缺省逻辑扩展的子集.同时,还存在贪婪缺省理论(T,Δ)的某一GD-扩展,该GD-扩展不包含缺省理论的任一扩展.因此缺省逻辑和贪婪缺省逻辑是两种不同的逻辑.
关键词: 缺省逻辑     扩展     GD-扩展     伪子公式     Gentzen系统    
Greedy Default Logic
CHEN Bo1,2, CAO Cun-Gen1, SUI Yue-Fei1    
1. Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, The Chinese Academy of Sciences, Bejing 100190, China;
2. Shandong Electric Power Research Institute, State Grid Corporation of China, Ji'nan 250001, China
Foundation item: Special Fund for Agro-Scientific Research in the Public Interest (201303107)
Abstract: A greedy default logic is proposed in this paper, in which pseudo extensions is defined with aim of keeping as much information of the defaults as possible. The paper proves that a GD-extension of a default theory (T, Δ) in the greedy default logic may not be any extension of the default theory, and vice versa. An extension of the default theory may be a subset of a pseudo extension of a default theory (T, Δ) in the greedy default. Hence, the default logic, the greedy default logic and the greedier default logic are different logics.
Key words: default logic     extension     GD-extension     pseudo-formula     Gentzen system    

在经典逻辑中, 推理是单调的, 即在已知的前提中添加新的信息, 不会使其推导出的集合缩小.与之相反, 非单调逻辑中, 推导关系(⊢)的单调性是不成立的.在已有的知识库中添加新的知识后, 可能会推翻之前的推论.即推导出的集合不会随着前提的增加而扩大.典型的非单调逻辑有缺省逻辑、封闭世界假设、限定推理(circumscription)和单调模态逻辑等.信念修正也可以被看作是一种非单调逻辑.

经典逻辑可以准确地表明一个事物为真还是为假, 但在现实世界中, 很多事物都是一般情况下为真, 但是有特殊情况的存在.比较经典的例子是“鸟通常会飞”, 在经典逻辑中, 我们只能将其表示为“所有的鸟都会飞”, 这显然是假的, 因为还有类似于鸵鸟等特例的存在.但是, 如果表示为“存在鸟会飞”又不符合我们想要表达的含义.因此, 我们必须表示为“除了鸵鸟、企鹅...之外, 所有的鸟都会飞”.缺省逻辑的目的在于形式化这样的推导规则.

缺省逻辑[1]是由Reiter于1980年首先提出来的, 是缺省推理的一种形式化方法.缺省逻辑中的缺省规则是基于假设的, 并且在许多领域有着广泛的应用[2].包括非单调继承网络(nonmonotomnic inheritance network)[3]、信息检索[4]和常识推理[5]等.在缺省规则中, 我们可以把上述情形形式化地表示为一个推导规则, 即“缺省的, 鸟会飞”, 不需要列出所有的例外.

缺省逻辑的语言是基于一阶逻辑的, 公式的定义在缺省逻辑与一阶逻辑中是相同的.一个缺省规则是形如$\frac{{Bird:Flying}}{{Flying}}$的表达式, 其含义为“缺省的, 鸟会飞”.一个缺省理论Γ是一个二元组(T, Δ), 其中, T是公式的集合, Δ是缺省规则的集合.缺省理论的扩展是缺省推理中重要的概念, 它由缺省理论和缺省推理定义.Ƚukaszewicz[6]给出了一种缺省逻辑的语义, 但在这种语义中, 缺省逻辑的模型实际上是满足扩展中所有一阶逻辑公式的模型, 并没有对缺省规则进行解释, 因此这种模型仍然是一阶逻辑的模型.

在实际应用方面, 缺省逻辑存在着一定的局限性.研究人员提出一些缺省逻辑的变体(variant)来获得某些特定的性质或者赋予扩展更为直观的解释, 亦或为了解决计算复杂度的问题.例如, 在使用缺省规则对知识库进行扩充时, 显式或者隐式地制定优先顺序[7]; 证实缺省逻辑(justified default logic)[8]和受限缺省逻辑(constrained default logic)[9]确保扩展的存在; 为了降低计算扩展的难度, 一些缺省逻辑的变体使用命题逻辑语言[10]、描述逻辑语言[11]以及OWL-DL语言[12]等可判定语言.近年来, 臧良俊还提出了分层的缺省逻辑[13]和分层的缺省描述逻辑[14], 将缺省规则由公式层面拓展到了规则层面, 为缺省逻辑引入了分层的概念.

考虑如下例子, 给定一个缺省理论(T, Δ), 其中, T={Man(Jone), ¬ HasArm(Jone)}, 表达某个人Jone没有胳膊; Δ由一个缺省规则$\frac{{{\rm{Man(}}x{\rm{)}}:{\rm{HasArm(}}x{\rm{)}} \wedge {\rm{HasLeg}}(x)}}{{{\rm{HasArm(}}x{\rm{)}} \wedge {\rm{HasLeg}}(x)}}$组成, 该缺省规则的含义是:缺省地, 人是有胳膊和腿的.在缺省逻辑中, 缺省理论(T, Δ)只有一个扩展${\rm{Th}}(\{ {\rm{Man(Jone)}}, \neg {\rm{HasArm(Jone)}}\})$, 即我们不能获得该人是否具有腿的信息.事实上, 我们希望能够从上述的缺省理论中推导出没有胳膊的Jone是缺省的有腿的.形式化地表示为由${\rm{Man(Jone)}}, \neg {\rm{HasArm(Jone)}}, \frac{{{\rm{Man(}}x{\rm{)}}:{\rm{HasArm(}}x{\rm{)}} \wedge {\rm{HasLeg}}(x)}}{{{\rm{HasArm(}}x{\rm{)}} \wedge {\rm{HasLeg}}(x)}}$缺省地推导出HasLeg(Jone).

本文将提出一种贪婪缺省逻辑, 使得在贪婪缺省逻辑中, 缺省理论的扩展(我们称其为GD-扩展)要尽可能地保留缺省规则中结论公式中所蕴含的信息.为了表达缺省理论中公式和扩展的关系, 参照子公式的概念, 我们引入了伪子公式的概念.并且, 一个公式的子公式一定是该公式的伪子公式, 反之, 结论不成立.例如, 上述的例子, 在贪婪缺省逻辑中, 我们会将公式q^r的伪子公式r添加到扩展中去, 即保留了公式q^r与{p, ¬ q}协调的部分.本文将给出贪婪缺省逻辑中的推导规则, 建立了贪婪缺省逻辑的推演系统—GD系统.类似于经典逻辑中的Gentzen推演系统[15], 缺省逻辑推演系统—GD系统的推导规则通过分解连接词的方法, 将每个缺省规则的结论部分拆分为原子公式或者原子公式的否定, 判断原子公式(原子公式的否定)是否保留或者删除, 将保留的原子公式(原子公式的否定)重新按照原有的连接词进行复合, 得到结论公式的伪子公式.本文给出了贪婪缺省逻辑扩展的构造方法, 并对贪婪缺省逻辑的扩展和缺省逻辑的GD-扩展进行了比较, 证明了如果一个缺省理论存在扩展E, 则存在一个GD-扩展E′, 使得EE′.反之不成立.

本文第1节给出缺省逻辑的基本定义和伪公式的定义.第2节给出贪婪缺省逻辑的推演系统—GD系统.第3节讨论贪婪缺省逻辑的推演系统—GD系统的性质.第4节通过例子对贪婪缺省逻辑的扩展(即GD-扩展)和缺省逻辑的扩展进行比较.第5节总结全文.

1 研究框架

为了简化讨论, 我们使用命题逻辑的语言作为缺省逻辑的语言.

定义1.1. 给定命题逻辑的语言L, L包含下列符号.

● 命题变量:p0, p1, …;

● 逻辑连接词:¬ , ∧ , ∨ .

公式定义如下:

$ \phi = p|\neg p|{\phi _1} \wedge {\phi _2}|{\phi _1} \vee {\phi _2}. $

在本文中, 否定连接词“¬ ”仅出现在原子公式的前面.因为由德摩根律, 我们可以将一般公式化简为否定连接词限定只能出现在原子公式前的形式.

模型M是一个赋值v.我们称公式Φ在模型M下是可满足的, 记为${\boldsymbol{\rm{M}}} \models \phi $, 如果

$ \left\{ \begin{array}{l} v(p) = 1,\;\;\;\;\;如果\phi = p\\ v(p) = 0,\;\;\;\;\;如果\phi = \neg p\\ {\boldsymbol{\rm{M}}} \models {\phi _1}{\boldsymbol{\rm{并且M}}} \models {\phi _2},{\rm{如果}}\phi = {\phi _1} \wedge {\phi _2}\\ {\boldsymbol{\rm{M}}} \models {\phi _1}{\boldsymbol{\rm{或者M}}} \models {\phi _2},{\rm{如果}}\phi = {\phi _1} \vee {\phi _2} \end{array} \right.. $

定义1.2(缺省规则). 缺省规则δ是形如$\frac{{\phi :{\psi _1}, ..., {\psi _n}}}{\chi }$的表达式, 其中,

●  Φ, ψ1, ..., ψn, χ为公式;

●  Φ称为δ的前提条件, 记为pre(δ);

●  ψ1, ..., ψn称为δ的检验条件, 记为just(δ);

●  χ称为δ的结论, 记为cons(δ).

一个缺省规则δ是正则的, 如果δ形如$\frac{{\phi :\psi }}{\psi }, $通常, 为了便于表示, 我们记为$\phi \rightsquigarrow \psi.$

定义1.3(缺省理论). 缺省理论Γ是一个二元组(T, Δ), 其中, T是公式的集合, Δ是缺省规则的集合.如果Δ中的缺省规则都是正则的, 则称缺省理论Γ=(T, Δ)为正则缺省理论.

定义1.4(∧ Γ演算). 给定缺省理论Γ=(T, Δ), A是公式的集合, ∧ Γ(A)是满足下列条件的最小集合.

● ${ \wedge _\Gamma }1).\; T \subseteq { \wedge _\Gamma }(A); $

● ${ \wedge _\Gamma }2).\; Th({ \wedge _\Gamma }(A)) = { \wedge _\Gamma }(A); $

● ${ \wedge _\Gamma }3).$对于任意的$\delta = \frac{{\phi :{\psi _1}, ..., {\psi _n}}}{\chi } \in \Delta, $如果$\phi \in { \wedge _\Gamma }(A)$, $\neg {\psi _1}\not \in A, ..., \neg {\psi _n}\not \in A, $$\chi \in { \wedge _\Gamma }(A).$

Th(A)表示A的理论闭包.

定义1.5(扩展). 给定缺省理论Γ和一个公式集合E, 如果E是∧ r的固定点, 即E=∧ r(E), 则称EΓ的一个扩展.

定义1.6. 给定公式的集合E和缺省理论Γ=(T, Δ).定义

E_0=T,

${E_{i + 1}} = Th({E_i}) \cup \left\{ {\chi |\frac{{\phi :{\psi _1}, ..., {\psi _n}}}{\chi } \in \Delta, \phi \in {E_i}, \neg {\psi _1}, ..., \neg {\psi _n}\not \in E} \right\}, $

E是缺省理论Γ=(T, Δ)的扩展当且仅当$E = \bigcup\limits_{i = 0}^\infty {{E_i}}.$

定义1.7(子公式). 给定公式Φ, 公式ψΦ的子公式, 记作ψΦ, 如果Φ=ψ或者

(ⅰ)如果ΦΦ1, 则ψΦ1;

(ⅱ)如果Φ=Φ1Φ2Φ1Φ2, 则ψΦ1ψΦ2.

Φ=(pq)∧ (rs), 则有pq, rsΦpr, qr, p∧ (rs)≤Φ.

为了区分形如pr, qr, p∧ (rs)这种既是公式Φ的一部分, 但又不是Φ的子公式的公式, 我们引入伪子公式的概念.

定理1.8(伪子公式). 给定公式Φ[ψ1, …, ψn], 其中, ψiψiΦ中的一次出现, 令公式ψ=Φ[ψ1/λ, ..., ψn/λ], 即将Φ中的ψi替换为空公式λ, 我们称ψΦ的伪子公式, 记作$\psi \subseteq \phi.$ψΦ的伪子公式, 如果$\psi \subseteq \phi $$\psi \ne \phi.$

Φ=(pq)∧ (rs), 则有pq, rs, pr, qr, p∧ (rs)⊆ Φ.

命题1.9. 给定公式Φ1, Φ2, ψ1ψ2,

(ⅰ) ψ1Φ1蕴含ψ1Φ1Φ2并且ψ1Φ1Φ2;

(ⅱ) ψ1Φ1ψ2Φ2蕴含¬ ψ1⊆ ¬ Φ1, ψ1ψ2Φ1Φ2ψ1ψ2Φ1Φ2.

命题1.10. 对于任意公式Φψ, 如果ψΦ, 则ψΦ.

命题1.11.  ≤和⊆ 是定义在公式集合上的偏序关系.

给定公式Φ, 令P(Φ)为Φ的所有伪子公式构成的集合.每一个公式ψP(Φ)都由一个集合t(ψ)={[p1], ..., [pn]}来决定, 其中, [pi]是原子公式piΦ中的一次出现, 满足ψ=Φ([p1]/λ, …, [pn]/λ).

给定任意ψ1, ψ2P(Φ), 定义:

$ \begin{array}{l} {\psi _1} \cap {\psi _2} = \max \{ \psi :\psi \subseteq {\psi _1}, \psi \subseteq {\psi _2}\} ;\\ {\psi _1} \cup {\psi _2} = \min \{ \psi :\psi \supseteq {\psi _1}, \psi \supseteq {\psi _2}\} . \end{array} $

命题1.12. 对于任意的伪子公式ψ1, ψ2P(Φ), ψ1ψ2ψ1ψ2都是存在的.P(Φ)=(P(Φ), ∪ , ∩ , Φ, λ)是具有最大元Φ和最小元λ的格.

命题1.13. 对于任意的伪子公式ψ1, ψ2P(Φ), ψ1ψ2当且仅当τ(ψ1)⊇ τ(ψ2), 并且有

$ \begin{array}{l} \tau ({\psi _1} \cap {\psi _2}) = \tau ({\psi _1}) \cup \tau ({\psi _2});\\ \tau ({\psi _1} \cup {\psi _2}) = \tau ({\psi _1}) \cap \tau ({\psi _2}). \end{array} $
2 贪婪缺省推演系统—GD系统

在本节中, 我们考虑的缺省规则均为正则缺省规则.考虑缺省理论:Γ=(T, Δ), 其中,

$ \begin{align} & T=\{\text{Man(Jone)}, \neg \text{HasArm(Jone)}\}, \\ & \Delta =\{\text{Man}(x)\rightsquigarrow \text{HasLeg}(x)\wedge \text{HasArm}(x)\}. \\ \end{align} $

在经典缺省逻辑中, Γ的扩展为E=Th({Man(Jone), ¬ HasArm(Jone)}).我们从已知的缺省规则中不能获得更多的信息, 并且因为HasArm(Jone)∧ HasLeg(Jone)与¬ HasArm(Jone)矛盾而将HasLeg(Jone)也一同舍弃了.一般来说, 一个没有手的人是有腿的, 这是符合我们日常认知的.因此我们提出贪婪缺省逻辑, 使得在贪婪缺省逻辑中, E' =Th({Man(Jone), ¬ HasArm(Jone), HasLeg(Jone)})为缺省理论Γ的扩展(GD-扩展).

定义2.1. 缺省矢列式是形如T11T22的表达式.其中, T1, T2是公式的集合, Δ1, Δ2是缺省规则的序列.

表达式Δ1, δ, Δ2表示Δ2δ≤Δ1, 其中, Δ1和Δ2是缺省规则的序列, δ是缺省规则, 即Δ1中的缺省规则的序优于δ, 并且δ的序优于Δ2中的缺省规则.

缺省矢列式T1, δ, Δ2T, θ1, Δ2的含义为:缺省表达式T|D1, δ, D2可以通过作用缺省规则δ规约为T, θ1, Δ2.

在这里, 我们要求对于任意的公式Φ∈ pre(Δ1)pre(Δ1), $T\not \vdash \phi $; 并且$T \vdash $pre(δ).

在缺省逻辑中, 缺省规则作用的思路是:给定一个缺省规则$\phi \rightsquigarrow \psi $和公式集合T, 我们首先判断条件$T\vdash \phi $是否成立, 如果条件成立, 再判断ψT是否协调; 若协调, 则将ψ添加到集合T中去.因此, 改变现有集合T的是公式ψ而不是Φ.

如果将T看作是一个知识系统, 公式Φ可以看作是规则的启动条件, 它不对原有的系统的内容进行扩展.并且, 如果启动条件得到满足, 已有的知识与ψ不矛盾的话, 我们就可以将ψ作为一条新的知识添加到系统中去.但是, 如果ψ与原有的知识矛盾, 在缺省逻辑中我们会将ψ舍去.而缺省规则$\phi \rightsquigarrow \psi, $它实际上是一条经验规则, 其含义, 是当Φ成立时, 通常有ψ成立.公式ψ的结构也可能不是简单的原子公式, 而是通过逻辑连接词复合而成的复杂公式.正如上面的例子一样, 即使ψ在系统中不成立, 但ψ中可能还有一些与原系统不矛盾的信息, 因此, 我们希望能够通过分解连接词的方法, 尽可能地保留ψ中与T不矛盾的信息.

贪婪缺省推演系统—GD系统:推导规则.

在下列所有的推导规则中, T是公式集合, Δ1和Δ2是缺省规则的序列, 并且对于Δ1中的任意缺省规则$\delta =\phi \rightsquigarrow \psi, $都有$T\not \vdash \phi.$

定义2.2. Atomic+-rule:

$ \frac{T\vdash \phi \ \ T\not{\vdash }\neg p}{T|{{\Delta }_{1}}, \phi \rightsquigarrow p, {{\Delta }_{2}}\Rightarrow T, p|{{\Delta }_{1}}, {{\Delta }_{2}}}, \frac{T\vdash \phi \ \ T\not{\vdash }p}{T|{{\Delta }_{1}}, \phi \rightsquigarrow \neg p, {{\Delta }_{2}}\Rightarrow T, \neg p|{{\Delta }_{1}}, {{\Delta }_{2}}}. $

公式θ可能是属于T的, 但是我们仍记为$T|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow T, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}$来表示该θ是通过作用缺省规则产生的.

定义2.3. Atomic-rule:

$ \frac{T\vdash \phi \ \ T\vdash \neg p}{T|{{\Delta }_{1}}, \phi \rightsquigarrow p, {{\Delta }_{2}}\Rightarrow T, \lambda |{{\Delta }_{1}}, {{\Delta }_{2}}}, \frac{T\vdash \phi \ \ T\vdash p}{T|{{\Delta }_{1}}, \phi \rightsquigarrow \neg p, {{\Delta }_{2}}\Rightarrow T, \lambda |{{\Delta }_{1}}, {{\Delta }_{2}}}. $

原子公式和原子公式的否定形式是公式的最基本形式, 如果协调, 则将公式添加到集合T中去.如果不协调, 则表明T可以推导出公式的否定, 由于原子公式不能再继续分解, 因此将公式舍去.

定义2.4. -rule:

$ \frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ T, {{\psi }_{1}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}\wedge {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}. $

-rule是指对于缺省规则$\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, $如果$T\vdash \phi $成立, 集合T作用缺省规则$\phi \rightsquigarrow {{\psi }_{1}}$可以得到$T\cup \{{{\psi }_{1}}\}, T\cup \{{{\psi }_{1}}\}$作用缺省规则$\phi \rightsquigarrow {{\psi }_{2}}$可以得到$T\cup \{{{\psi }_{1}}, {{\psi }_{2}}\}, $则集合T作用缺省规则$\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}$可以得到$T\cup \{{{\psi }_{1}}\wedge {{\psi }_{2}}\}.$

事实上, ∧ -rule还有另外一种形式:

$ \frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ T, {{\psi }_{2}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}\wedge {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}. $

即如果$T\vdash \phi $成立, 集合T作用缺省规则$\phi \rightsquigarrow {{\psi }_{1}}$可以得到$T\cup \{{{\psi }_{2}}\}, T\cup \{{{\psi }_{2}}\}$作用缺省规则$\phi \rightsquigarrow {{\psi }_{1}}$可以得到$T\cup \{{{\psi }_{1}}, {{\psi }_{2}}\}, $则集合T作用缺省规则$\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}$可以得到$T\cup \{{{\psi }_{1}}\wedge {{\psi }_{2}}\}.$因为对于集合T和公式\[{{\psi }_{1}}, {{\psi }_{2}}, T\cup \{{{\psi }_{1}}, {{\psi }_{2}}\}\]是协调的, 所以这两条规则是等价的, 我们只保留其中的一条.并且, 我们在之后的定理中也证明, 如果ψ可以全部保留, 则ψ与集合T是协调的.

定义2.5. ∧ -rule:

$ \begin{align} &\frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ T, {{\theta }_{1}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{1}}, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{1}}\wedge {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ &\frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ T, {{\theta }_{2}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{2}}, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{1}}\wedge {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ \end{align} $

其中, θ1θ2分别是ψ1ψ2的伪子公式.

在∧ -rule中, 缺省规则$\phi \rightsquigarrow \psi $作用在集合T上得到的是ψ的一个伪子公式.这说明, ψ本身与集合T是不协调的.ψ的最外层逻辑联结词是合取符号, 即ψ=ψ1ψ2.于是有ψ1ψ2T是不协调的, 缺省规则$\phi \rightsquigarrow {{\psi }_{1}}$$\phi \rightsquigarrow {{\psi }_{2}}$作用的顺序不同, 则可能产生的伪子公式不同.例如, 最简单的情况, 令$T=\{p\}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}=p\rightsquigarrow q\wedge \neg q.$先作用$p\rightsquigarrow q$产生的集合为{p, q}, 而先作用$p\rightsquigarrow \neg q$产生的集合为$\{p, \neg q\}.$

所以上述规则并不是等价的, 需要一一列出.

定义2.6. ∨ -rule:

$ \begin{align} & \frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}\vee {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ & \frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\psi }_{1}}\vee {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}. \\ \end{align} $

在∨ -rule中, 如果Tψ1或者ψ2是协调的, 则Tψ1ψ2是协调的.因此只要满足上述条件之一, 我们即可把ψ1ψ2添加到T当中去.即当ψ与集合T是协调的, 则将ψ全部保留.

定义2.7. ∨ -rule:

$ \frac{T\vdash \phi \ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{T|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow T|{{\Delta }_{1}}, {{\Delta }_{2}}}, $

其中, θ1θ2分别是ψ1ψ2的真伪子公式.

在∨ -rule中, 公式ψ1ψ2与集合T是不协调的.因此公式ψ1ψ2与集合T都是不协调的.即集合T作用$\phi \rightsquigarrow {{\psi }_{1}}$$\phi \rightsquigarrow {{\psi }_{2}}$产生的新公式都是ψ1ψ2的伪子公式, 考虑到公式ψ1ψ2与集合T都是不协调的, 我们不将

任何公式添加到$T$中去.

定义2.8. TR-rule:

$ \frac{{{T}_{1}}|{{\Delta }_{1}}\Rightarrow {{T}_{2}}|{{\Delta }_{2}}\ \ {{T}_{2}}|{{\Delta }_{2}}\Rightarrow {{T}_{3}}|{{\Delta }_{3}}}{{{T}_{1}}|{{\Delta }_{1}}\Rightarrow {{T}_{3}}|{{\Delta }_{3}}}. $

直观上, TR-rule表明缺省矢列式是具有传递性的, 即如果矢列式T11T22成立, 且有T22T33成立, 则有T11T33成立.

定义2.9(证明). 给定公式的集合S1S2, 缺省规则的集合Δ1和Δ22可能是∅ ).我们称缺省矢列式S11S22是GD-可证的, 记为${{\vdash }^{\mathbf{GD}}}{{S}_{1}}|{{\Delta }_{1}}\Rightarrow {{S}_{2}}|{{\Delta }_{2}}$, 当且仅当存在一棵以S11S22为根节点的证明树T, 满足:

1) T的非叶节点都是缺省矢列式;

2) T的所有叶节点都是Axiom的上层;

3) T中除了根节点以外的所有节点都是某一个推导规则的上层, 且其直接后继节点为该缺省规则的下层.

显然, 证明树T的任意子树也是证明树.

例如:给定缺省理论$\Gamma =(T, \Delta), $其中, $T=\{p\}, \Delta =\{p\rightsquigarrow q, q\rightsquigarrow r\}, $

$ \frac{\frac{T\vdash p\ \ T\not{\vdash }\neg q}{p|p\rightsquigarrow q, q\rightsquigarrow r\Rightarrow p, q|q\rightsquigarrow r}\ \ \frac{p, q\vdash q\ \ p, q\not{\vdash }\neg r}{p, q|q\rightsquigarrow r\Rightarrow p, q, r}}{T|p\rightsquigarrow q, q\rightsquigarrow r\Rightarrow p, q, r} $

T|Δ⇒ p, q, r的一棵证明树, 即T|Δ⇒ p, q, r是可证的.

命题2.10. 给定缺省矢列式S11S22, 如果S11S22是GD-可证的, 则有Δ2⊆ Δ1, S1S2.

定义2.11(公式的序L下可证性). 给定缺省理论Γ=(T, Δ)和一个定义在Δ上的全序L, 其中, L=δ1, δ2, ..., δn, ....公式ψ是关于缺省理论Γ=(T, Δ)在序L下可证的, 如果存在一个Δ中的缺省规则的序列${{{\delta }'}_{1}}, {{{\delta }'}_{2}}, …, {{{\delta }'}_{j}}$, 使得:

$ {{\vdash }^{\mathbf{GD}}}{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{{\delta }'}_{1}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, {{\theta }_{1}}|{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}, $

$ {{\vdash }^{\mathbf{GD}}}{{T}_{i-1}}|{{\Delta }_{i-{{1}^{\prime }}}}, {{{\delta }'}_{i}}, {{\Delta }_{i-{{1}^{\prime \prime }}}}\Rightarrow {{T}_{i-1}}, {{\theta }_{i}}|{{\Delta }_{i-{{1}^{\prime }}}}, {{\Delta }_{i-{{1}^{\prime \prime }}}}, $

$ {{\vdash }^{\mathbf{GD}}}{{T}_{j-1}}|{{\Delta }_{j-{{1}^{\prime }}}}, {{{\delta }'}_{1}}, {{\Delta }_{j-{{1}^{\prime \prime }}}}\Rightarrow {{T}_{j-1}}, {{\theta }_{j}}|{{\Delta }_{j-{{1}^{\prime }}}}, {{\Delta }_{j-{{1}^{\prime \prime }}}}, $
$ {{T}_{j}}\vdash \psi, $

其中, ${{\Delta }_{0}}=\Delta ={{\Delta }_{{{0}'}}}\cup {{\Delta }_{{{0}''}}}, {{\Delta }_{i}}={{\Delta }_{i-1}}-\{{{\delta }_{{{i}'}}}\}={{\Delta }_{{{i}'}}}\cup {{\Delta }_{{{i}''}}}; $对于任意的缺省规则$\delta \in {{\Delta }_{{{i}'}}}, $$\delta {{\ge }^{L}}{{\delta }_{i+{{1}^{\prime }}}}$并且${{T}_{i}}\not{\vdash }\text{pre}(\delta); $同时, 对于任意的缺省规则$\delta \in {{\Delta }_{{{i}''}}}, $都有${{\delta }_{i+{1}'}}{{\ge }^{L}}\delta.$

从公式的可证性我们了解到, 缺省规则的作用依赖于给定的严格偏序, 每一步作用的缺省规则都是活动的, 并且具有最优先的序.在每次作用完之后, 我们就将这个缺省规则从原有的集合中移除.我们要求每一步的矢列式都是缺省可证的, 并且由这些矢列式组成了一个连续可证的缺省矢列式的序列, 使得可证的公式可以被矢列式当中的某一个集合T' 推导出来.这样按照严格偏序去一步一步地作用缺省规则而生成的公式, 都是在该序下关于缺省理论Γ可证的公式, 那么包含所有这些公式的集合, 我们定义为GD-扩展, 定义如下.

定义2.12(GD-扩展). 给定缺省理论Γ=(T, Δ), 其中, T是协调的公式集合, Δ是缺省规则的集合.公式的集合E是缺省理论Γ=(T, Δ)的一个GD-扩展, 如果存在一个Δ上的全序L=δ0, δ1, δ2, …, δi, …, 使得

$ {{\vdash }^{\mathbf{GD}}}{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{{\delta }'}_{1}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, {{\theta }_{1}}|{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}, $

$ {{\vdash }^{\mathbf{GD}}}{{T}_{i-1}}|{{\Delta }_{i-{{1}^{\prime }}}}, {{{\delta }'}_{i}}, {{\Delta }_{i-{{1}^{\prime \prime }}}}\Rightarrow {{T}_{i-1}}, {{\theta }_{i}}|{{\Delta }_{i-{{1}^{\prime }}}}, {{\Delta }_{i-{{1}^{\prime \prime }}}}, $

$ E=Th\left( \bigcup\limits_{i=0}^{\infty }{{{T}_{i}}} \right), $

其中, ${{T}_{0}}=T, {{T}_{i}}={{T}_{i-1}}\cup \{{{\theta }_{i}}\}; $${{\Delta }_{0}}=\Delta ={{\Delta }_{{{0}'}}}\cup {{\Delta }_{{{0}''}}}, {{\Delta }_{i}}={{\Delta }_{i-1}}-\{{{\delta }_{{{i}'}}}\}={{\Delta }_{{{i}'}}}\cup {{\Delta }_{{{i}''}}}; $对于任意的缺省规则$\delta \in {{\Delta }_{i-{1}'}}, $$\delta {{\ge }^{L}}{{\delta }_{{{i}'}}}, $并且${{T}_{i-1}}\not{\vdash }$pre(δ); 同时, 对于任意的缺省规则$\delta \in {{\Delta }_{i-{1}''}}, $都有${{\delta }_{{{i}'}}}{{\ge }^{L}}\delta.$

我们称E是缺省理论Γ=(T, Δ)的一个关于序L的GD-扩展.并且, 对于任意公式$\phi \in \text{pre}\left(\bigcap\limits_{i=0}^{\infty }{{{\Delta }_{i}}} \right), E\not{\vdash }\phi.$

不同于缺省逻辑, 贪婪缺省逻辑的GD-扩展的定义是构造型的.在贪婪缺省逻辑中, 由于随着作用集合的变化, 作用相同的缺省规则产生的伪子公式是不尽相同的; 即便是将缺省规则作用在最终生成的GD-扩展上所生成的公式与在生成扩展的过程中作用于该规则所产生的公式也未必相同.而在缺省逻辑中, 即使集合发生变化, 作用相同的缺省规则产生的公式要么是其本身, 要么是一个空公式; 并且, 将缺省规则作用在最终生成的扩展上生成的公式与在生成扩展的过程中作用于该规则上产生的公式是相同的.因此, 我们不能把GD-扩展不动点型定义为类似于缺省逻辑中形式, 即${{\wedge }_{\Gamma }}(S)=Th(T\cup \{\phi :S\vdash \phi, E\not{\vdash }\neg \psi, \phi \rightsquigarrow \psi \in \Delta \}), $其中, E是扩展.

例2.13:给定缺省理论Γ=(T, Δ), $T=\{{{p}_{1}}, \neg {{p}_{2}}\}, \Delta =\{{{p}_{3}}\rightsquigarrow {{p}_{4}}, {{p}_{1}}\rightsquigarrow {{p}_{2}}\wedge {{p}_{3}}, {{p}_{4}}\rightsquigarrow {{p}_{2}}\}.$L是定义在Δ上的全序, 其中, $L={{p}_{3}}\rightsquigarrow {{p}_{4}}, {{p}_{1}}\rightsquigarrow {{p}_{2}}\wedge {{p}_{3}}, {{p}_{4}}\rightsquigarrow {{p}_{2}}.$我们构造缺省理论Γ=(T, Δ)的一个关于序L的GD-扩展如下.

Step 1.

$ {{T}_{0}}=T, {{\Delta }_{0}}=\Delta ;{{\delta }_{{{k}_{0}}}}={{p}_{1}}\rightsquigarrow {{p}_{2}}\wedge {{p}_{3}}, {{\Delta }_{{{0}'}}}=\{{{p}_{3}}\rightsquigarrow {{p}_{4}}\}, {{\Delta }_{{{0}''}}}=\{{{p}_{4}}\rightsquigarrow {{p}_{2}}\}; $

因为

$ \frac{\frac{{{T}_{0}}\vdash {{p}_{1}}\ \ {{T}_{0}}\vdash \neg {{p}_{2}}}{{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{p}_{1}}\rightsquigarrow {{p}_{2}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, \lambda |{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}}\ \ \ \ \frac{{{T}_{0}}\vdash {{p}_{1}}\ \ {{T}_{0}}\not{\vdash }\neg {{p}_{3}}}{{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{p}_{1}}\rightsquigarrow {{p}_{3}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, {{p}_{3}}|{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}}}{{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{p}_{1}}\rightsquigarrow {{p}_{2}}\wedge {{p}_{3}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, {{p}_{3}}|{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}}, $

故而有${{\vdash }^{\mathbf{D}}}{{T}_{0}}|{{\Delta }_{{{0}'}}}, {{\delta }_{{{k}_{0}}}}, {{\Delta }_{{{0}''}}}\Rightarrow {{T}_{0}}, {{\theta }_{{{k}_{0}}}}|{{\Delta }_{{{0}'}}}, {{\Delta }_{{{0}''}}}$, 其中, ${{\theta }_{{{k}_{0}}}}={{p}_{3}}.$

Step 2.

$ {{\Delta }_{1}}={{\Delta }_{{{0}'}}}\cup {{\Delta }_{{{0}''}}}=\{{{p}_{3}}\rightsquigarrow {{p}_{4}}, {{p}_{4}}\rightsquigarrow {{p}_{2}}\}, {{T}_{1}}={{T}_{0}}\cup \{{{\theta }_{{{k}_{0}}}}\};{{\delta }_{{{k}_{1}}}}={{p}_{3}}\rightsquigarrow {{p}_{4}}, {{\Delta }_{{{1}'}}}\\=\varnothing, {{\Delta }_{{{0}''}}}=\{{{p}_{4}}\rightsquigarrow {{p}_{2}}\}; $

因为

$ \frac{{{T}_{1}}\vdash {{p}_{3}}\ \ {{T}_{1}}\not{\vdash }\neg \neg {{p}_{4}}}{{{T}_{1}}|{{p}_{3}}\rightsquigarrow {{p}_{4}}, {{\Delta }_{{{1}''}}}\Rightarrow {{T}_{1}}, {{p}_{4}}|{{\Delta }_{{{1}''}}}}, $

故而有${{\vdash }^{\mathbf{D}}}{{T}_{1}}|{{p}_{3}}\rightsquigarrow {{p}_{4}}, {{\Delta }_{{{1}''}}}\Rightarrow {{T}_{1}}, {{p}_{4}}|{{\Delta }_{{{1}''}}}, $其中, ${{\theta }_{{{k}_{1}}}}={{p}_{4}}.$

Step 3.

$ {{\Delta }_{2}}={{\Delta }_{{{0}'}}}\cup {{\Delta }_{{{0}''}}}=\{{{p}_{4}}\rightsquigarrow {{p}_{2}}\}, {{T}_{2}}={{T}_{1}}\cup \{{{\theta }_{{{k}_{1}}}}\};{{\delta }_{{{k}_{2}}}}={{p}_{4}}\rightsquigarrow {{p}_{2}}, {{\Delta }_{{{1}'}}}=\varnothing, {{\Delta }_{{{0}''}}}=\varnothing ; $

因为

$ \frac{{{T}_{2}}\vdash {{p}_{4}}\ \ {{T}_{2}}\vdash \neg {{p}_{2}}}{{{T}_{2}}|{{p}_{4}}\rightsquigarrow {{p}_{2}}\Rightarrow {{T}_{2}}, \lambda }, $

故而有${{\vdash }^{\mathbf{D}}}{{T}_{2}}|{{p}_{4}}\rightsquigarrow {{p}_{2}}\Rightarrow {{T}_{2}}, \lambda, $其中, ${{\theta }_{{{k}_{2}}}}=\lambda.$

故而Th(T2)是缺省理论Γ=(T, Δ)的一个关于序L的GD-扩展, 并且公式p3, p4都是于缺省理论Γ=(T, Δ)在序λ下可证的.

3 贪婪缺省推演系统-GD系统的性质

例3.1:给定公式集合$S=\{p, \neg {{q}_{2}}, \neg {{q}_{4}}\}$和缺省规则$\delta =p\rightsquigarrow ({{q}_{1}}\wedge {{q}_{2}})\wedge ({{q}_{3}}\wedge {{q}_{4}}).$首先, 因为$S\vdash p, $缺省规则δ是可作用于集合S上的; 之后, 按照贪婪缺省逻辑的推导规则, 将缺省规则δ作用在集合S上.

$ \frac{\frac{\frac{S\vdash p\ \ S\not{\vdash }\neg {{q}_{1}}}{S|p\rightsquigarrow {{q}_{1}}\Rightarrow S, {{q}_{1}}}\ \ \frac{S\vdash p\ \ S\vdash \neg {{q}_{2}}}{S, {{q}_{1}}|p\rightsquigarrow {{q}_{2}}\Rightarrow S, {{q}_{1}}, \lambda }}{S|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}\Rightarrow S, {{q}_{1}}}\ \ \frac{\frac{S\vdash p\ \ S\not{\vdash }\neg {{q}_{3}}}{S|p\rightsquigarrow {{q}_{3}}\Rightarrow S, {{q}_{3}}}\ \ \frac{S\vdash p\ \ S\vdash \neg {{q}_{4}}}{S, {{q}_{3}}|p\rightsquigarrow {{q}_{4}}\Rightarrow S, {{q}_{3}}, \lambda }}{S|p\rightsquigarrow {{q}_{3}}\wedge {{q}_{4}}\Rightarrow S, {{q}_{3}}}}{S|p\rightsquigarrow ({{q}_{1}}\wedge {{q}_{2}})\wedge ({{q}_{3}}\wedge {{q}_{4}})\Rightarrow S, {{q}_{1}}\wedge {{q}_{3}}}. $

我们可以得到公式q1q3.q1q3并不是(q1q2)∧ (q3q4)的子公式, 而是(q1q2)∧ (q3q4)的伪子公式.

从上述的例子中我们发现, 在贪婪缺省逻辑中, 作用缺省规则δ而产生的公式是cons(δ)的伪子公式.正如接下来的定理3.2.

定理3.2.  给定协调的公式集合S, 缺省规则集合Δ1, Δ2和缺省规则$\delta =\phi \rightsquigarrow \psi; $其中, 对于任意的公式${{\phi }_{1}}\in \text{pre}({{\Delta }_{1}}), $都有$S\not{\vdash }{{\phi }_{1}}$.那么, 如果$S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}$是GD-可证的, 则θψ的伪子公式.

证明:我们对公式ψ的结构进行归纳证明.

基始:如果ψ=p或者ψp, 根据推导规则的定义, θ的形式要么是ψ本身, 要么是空公式.显然, ψ和空公式λ都是ψ的伪子公式, 结论成立.

归纳步骤:假设结论在结构比公式ψ简单的公式上成立.

如果${{\vdash }^{\mathbf{GD}}}S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}, $根据证明的定义, 存在一棵以$S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}$为根节点的证明树.那么存在以下几种情形.

情形1:ψ=ψ1ψ2.

根据证明树的定义, 证明树的最低两层有以下3种可能:

$ \begin{align} & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S|{{\Delta }_{1}}, {{\Delta }_{2}}}. \\ \end{align} $

对于第1种和第2种可能, 显然, ψ1ψ2是其本身的伪子公式, 结论成立.第3种情形是一种特殊的情形, 空公式是所有公式的伪子公式.

情形2:ψ=ψ1ψ2.

根据证明树的定义, 证明树的最低两层有以下3种可能:

$ \begin{align} & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ S, {{\psi }_{1}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}, {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\psi }_{1}}\wedge {{\psi }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ S, {{\theta }_{1}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}, \\ & \frac{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}\ \ S, {{\theta }_{2}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{2}}, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}}{S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}}. \\ \end{align} $

对于第1种情形, 显然, ψ1ψ2是其本身的伪子公式, 结论成立.我们下面将对第2种情形进行讨论.

因为缺省矢列式$S|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{1}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}|{{\Delta }_{1}}, {{\Delta }_{2}}$$S, {{\theta }_{1}}|{{\Delta }_{1}}, \phi \rightsquigarrow {{\psi }_{2}}, {{\Delta }_{2}}\Rightarrow S, {{\theta }_{1}}, {{\theta }_{2}}|{{\Delta }_{1}}, {{\Delta }_{2}}$都是GD-可证的; 由归纳假设, θ1θ2分别是ψ1ψ2的伪子公式.根据证明树的定义, θ=θ1θ2.又根据伪子公式的定义, θ1θ2ψ1ψ2的伪子公式, 故而结论成立.

第3种情形与第2种类似.

定理3.3. 给定协调的公式集合S, 缺省规则集合Δ1, Δ2和缺省规则$\delta =\phi \rightsquigarrow \psi; $其中, 对于任意的公式${{\phi }_{1}}\in \text{pre}({{\Delta }_{1}}), $都有$S\not{\vdash }{{\phi }_{1}}.$那么, $S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, \psi |{{\Delta }_{1}}, {{\Delta }_{2}}$是GD-可证的, 当且仅当$S\vdash \phi, $并且$S\not{\vdash }\neg \psi.$

证明:我们对公式ψ的结构进行归纳证明.

基始:如果ψ=p或者Φp, 根据推导规则的定义, 结论成立.

归纳步骤:假设结论在结构比公式ψ简单的公式上成立.

情形1:ψ=ψ1ψ2.

(⇒ )如果S|δS, ψ是可证的, 则存在一棵以S|δS, ψ为根节点的证明树, 使得该证明树的最底部的两层为

$ \frac{S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}}或者\frac{S|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\psi }_{2}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}}. $

根据证明的定义, 可以得到矢列式$S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}$或者$S|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\psi }_{2}}$是可证的.由归纳假设$S\cup \{{{\psi }_{1}}\}$或者$S\cup \{{{\psi }_{2}}\}$是协调的.因此$S\cup \{{{\psi }_{1}}\vee {{\psi }_{2}}\}$是协调的.即$S\not{\vdash }\neg \psi.$

(⇐ )如果$S\not{\vdash }\neg \psi, $则有$S\not{\vdash }\neg {{\psi }_{1}}\wedge \neg {{\psi }_{2}}.$$S\not{\vdash }\neg {{\psi }_{1}}$或者$S\not{\vdash }\neg {{\psi }_{2}}.$不妨假设$S\not{\vdash }\neg {{\psi }_{1}}.$由归纳假设, $S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}$是可证的.故而由推导规则∨ , 有

$ \frac{S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}}. $

可以知道, $S|\phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}$是可证的.同样地, 如果$S\not{\vdash }\neg {{\psi }_{2}}, $则有$S|\phi \rightsquigarrow {{\psi }_{1}}\vee {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\vee {{\psi }_{2}}$是可证的.

即结论在情形1的情况下成立.

情形2:ψ=ψ1ψ2.

(⇒ )如果S|δS, ψ是可证的, 则存在一棵以$S|\delta \Rightarrow S, \psi $为根节点的证明树, 使得该证明树的最底两层为

$ \frac{S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}\ \ S, {{\psi }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}, {{\psi }_{2}}}{S|\phi \rightsquigarrow \psi \Rightarrow S, {{\psi }_{1}}\wedge {{\psi }_{2}}}. $

根据证明树的定义, $S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}$是可证的, 由归纳假设可知$S\cup \{{{\psi }_{1}}\}$是协调的.同理, $S, {{\psi }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow $S, ψ1, ψ2也是可证的, 再次使用归纳假设可知, $S\cup \{{{\psi }_{1}}\}\cup \{{{\psi }_{2}}\}$是协调的.因此, $S\cup \{{{\psi }_{1}}\wedge {{\psi }_{2}}\}$是协调的, 故而$S\not{\vdash }\neg \psi.$

(⇐ )如果$S\not{\vdash }\neg \psi, $$S\not{\vdash }\neg {{\psi }_{1}}\vee \neg {{\psi }_{2}}.$$S\not{\vdash }\neg {{\psi }_{1}}$$S\not{\vdash }\neg {{\psi }_{2}}.$因为$S\cup \{{{\psi }_{1}}, {{\psi }_{2}}\}$是协调的, 所以, $S, {{\psi }_{1}}\not{\vdash }\neg {{\psi }_{2}}.$由归纳假设, $S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}$$S, {{\psi }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}, {{\psi }_{2}}$都是可证的.使用推导规则∧ , 有

$ \frac{S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\psi }_{1}}\ \ S, {{\psi }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}, {{\psi }_{2}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\wedge {{\psi }_{2}}}, $

可知$S|\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}\Rightarrow S, {{\psi }_{1}}\wedge {{\psi }_{2}}$是可证的.

即结论在情形2的情况下成立.

定理3.4. 给定协调的公式集合S, 缺省规则集合Δ1, Δ2和缺省规则$\delta =\phi \rightsquigarrow \psi; $其中, 对于任意的公式${{\phi }_{1}}\in \text{pre}({{\Delta }_{1}}), $都有$S\not{\vdash }{{\phi }_{1}}.$如果$S|{{\Delta }_{1}}, \phi \rightsquigarrow \psi, {{\Delta }_{2}}\Rightarrow S, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}$是GD-可证的, 则$S\cup \{\theta \}$是协调的.

证明:我们对ψ的公式结构进行归纳假设.

基始:如果ψ=p或者Φp, 由推导规则定义可知, 结论成立.

归纳步骤:假设结论在结构比公式ψ简单的公式上成立.

情形1:ψ=ψ1ψ2.

子情形1.1:q=ψ1ψ2,

由定理3.3可知, 结论成立.

子情形1.2:θ=λ, 结论成立.

情形2:ψ=ψ1ψ2.

子情形2.1:θ=θ1θ2.

如果$S|\phi \rightsquigarrow \psi \Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}$是可证的, 则存在一棵以$S|\phi \rightsquigarrow \psi \Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}$为根节点的证明树, 使得该证明树的最底两层为

$ \frac{S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\theta }_{1}}\ \ S, {{\theta }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\theta }_{1}}, {{\theta }_{2}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}\Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}} $ (1)
$ \frac{S|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\theta }_{2}}\ \ S, {{\theta }_{2}}|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\theta }_{2}}, {{\theta }_{1}}}{S|\phi \rightsquigarrow {{\psi }_{1}}\wedge {{\psi }_{2}}\Rightarrow S, {{\theta }_{1}}\wedge {{\theta }_{2}}} $ (2)

其中, 在公式(1) 中出现的θ1θ2与公式(2) 中出现的θ1θ2不一定相同.

由式(1) 可知, $S|\phi \rightsquigarrow {{\psi }_{1}}\Rightarrow S, {{\theta }_{1}}$是可证的, 故由归纳假设可知$S\cup \{{{\theta }_{1}}\}$是协调的.同理, $S, {{\theta }_{1}}|\phi \rightsquigarrow {{\psi }_{2}}\Rightarrow S, {{\theta }_{1}}, {{\theta }_{2}}$也是可证的, 因此, $S\cup \{{{\theta }_{1}}\}\cup \{{{\theta }_{2}}\}$是协调的.故而$S\cup \{{{\theta }_{1}}\wedge {{\theta }_{2}}\}$是协调的.

式(2) 的情形与式(1) 类似.

子情形2.2:θ=ψ1θ2θ=θ1ψ2.

与子情形2.1类似.

子情形2.3:θ=ψ1ψ2.

由定理3.3可知, 结论成立.

推论3.5. 给定缺省理论Γ=(T, Δ), 其中, T是协调的公式集合, Δ是缺省规则的集合.对于任意的公式集合E, 如果E是缺省理论Γ=(T, Δ)的一个GD-扩展, 则E是协调的.

证明:根据GD-扩展的定义, 我们对自然数n进行归纳.

基始:当n=0时, 由于T0=T, T是协调的, 因此$T_0$是协调的公式集合.结论成立.

归纳步骤:假设当$n=k$时, 结论成立, 即Tk是协调的公式集合.当n=k+1时, 令δ是序最优的, 并且是可以被作用的缺省规则.根据缺省规则的推导规则,

$ {{\vdash }^{\mathbf{GD}}}{{T}_{k}}|{{\Delta }_{1}}, \delta, {{\Delta }_{2}}\Rightarrow {{T}_{k}}, \theta |{{\Delta }_{1}}, {{\Delta }_{2}}, $

并且${{T}_{k+1}}={{T}_{k}}\cup \{\theta \}.$由定理3.4, Tk+1是协调的.并且根据GD-扩展的定义过程, 对于任意的自然数i, j, 如果ij, 则有TiTj.因此, $\bigcup\limits_{i=0}^{k+1}{{{T}_{i}}}={{T}_{k+1}}.$于是, 对于任意的自然数n, 都有Tn$\bigcup\limits_{i=0}^{n}{{{T}_{i}}}$均是协调的.又因为GD-扩展$E=Th\left(\bigcup\limits_{i=0}^{\infty }{{{T}_{i}}} \right), $因此E是协调的.

4 GD-扩展的性质及与扩展的比较

在第2节中, 我们给出了贪婪缺省逻辑中GD-扩展的定义.自然而然地, 我们会产生疑问, 对于缺省理论Γ, Γ在贪婪缺省逻辑中的GD-扩展E和缺省逻辑中的扩展E' 存在怎样的区别与联系呢?

可以发现, 贪婪缺省逻辑GD-扩展的定义与缺省逻辑扩展的构造定理是类似的, 且贪婪缺省逻辑的目标是尽可能地保留缺省规则中的信息.那么, 对于GD-扩展E, 是否存在扩展E' 使得E' ⊆ E?亦或对于扩展E' ,是否存在GD-扩展E使得E' ⊆ E?

首先, 回到本文开始部分提出的问题, Jone是一个没有腿的人和人是缺省的有胳膊并且有腿的; 其次, 我们使用贪婪缺省逻辑的推导规则, 是否可以得到我们想要的结果?

例4.1:给定缺省理论Γ=(T, Δ), 其中, $T=\{\text{Man(Jone)}, \neg \text{HasLeg(Jone)}\}$, $\Delta =\{\text{Man}(x)\rightsquigarrow \text{HasLeg}(x)\wedge \text{HasArm}(x)\}.$

构造关于缺省理论Γ的证明树如下:

$ \frac{\frac{T\vdash \text{Man(Jone)}\ \ T\vdash \neg \text{HasLeg(Jone)}}{T|\text{Man(Jone)}\rightsquigarrow \text{HasLeg(Jone)}\Rightarrow T, \lambda }\ \ \frac{T\vdash \text{Man(Jone)}\ \ T\not{\vdash }\neg \text{HasArm(Jone)}}{T, \lambda |\text{Man(Jone)}\rightsquigarrow \text{HasArm(Jone)}\Rightarrow T, \text{HasArm(Jone)}}}{T|\text{Man(Jone)}\rightsquigarrow \text{HasLeg(Jone)}\wedge \text{HasArm(Jone)}\Rightarrow T, \text{HasArm(Jone)}}. $

于是, 缺省理论的GD-扩展为Th({Man(Jone), ¬ HasLeg(Jone), HasArm(Jone)}).因此, 通过人是缺省的有胳膊和腿的这条规则以及Jone是一个没有腿的人推导出Jone是有胳膊而没有腿的.

下面我们将通过给出的几个具体例子来探讨贪婪缺省逻辑的扩展与缺省逻辑扩展之间的关系.

例4.2:给定缺省理论Γ=(T, Δ), T={p}, D={δ1, δ2}, 其中, ${{\delta }_{1}}=p\rightsquigarrow \neg {{q}_{1}}, {{\delta }_{2}}=p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}.$

我们可以写出两棵关于该缺省理论的证明树.

$ \frac{\frac{T\vdash p\ \ T\not{\vdash }{{q}_{1}}}{T|{{\delta }_{1}}, {{\delta }_{2}}\Rightarrow T, \neg {{q}_{1}}|{{\delta }_{2}}}\ \ \frac{\frac{T, \neg {{q}_{1}}\vdash p\ \ T, \neg {{q}_{1}}\vdash \neg {{q}_{1}}}{T, \neg {{q}_{1}}|p\rightsquigarrow {{q}_{1}}\Rightarrow T, \neg {{q}_{1}}}\ \ \frac{T, \neg {{q}_{1}}\vdash p\ \ T, \neg {{q}_{1}}\not{\vdash }\neg {{q}_{2}}}{T, \neg {{q}_{1}}|p\rightsquigarrow {{q}_{2}}\Rightarrow T, \neg {{q}_{1}}, {{q}_{2}}}}{T, \neg {{q}_{1}}|{{\delta }_{2}}\Rightarrow T, \neg {{q}_{1}}, {{q}_{2}}}}{T|{{\delta }_{1}}, {{\delta }_{2}}\Rightarrow T, \neg {{q}_{1}}, {{q}_{2}}}, $
$ \frac{\frac{\frac{T\vdash p\ \ T\not{\vdash }\neg {{q}_{1}}}{T|p\rightsquigarrow {{q}_{1}}, {{\delta }_{1}}\Rightarrow T, {{q}_{1}}|{{\delta }_{1}}}\ \ \frac{T, {{q}_{1}}\vdash p\ \ T, {{q}_{1}}\not{\vdash }\neg {{q}_{2}}}{T, {{q}_{1}}|p\rightsquigarrow {{q}_{2}}, {{\delta }_{1}}\Rightarrow T, {{q}_{1}}, {{q}_{2}}|{{\delta }_{1}}}}{T|{{\delta }_{2}}, {{\delta }_{1}}\Rightarrow T, {{q}_{1}}\wedge {{q}_{2}}|{{\delta }_{1}}}\ \ \frac{T, {{q}_{1}}\wedge {{q}_{2}}\vdash p\ \ T, {{q}_{1}}\wedge {{q}_{2}}\vdash {{q}_{1}}}{T, {{q}_{1}}\wedge {{q}_{2}}|{{\delta }_{1}}\Rightarrow T, {{q}_{1}}\wedge {{q}_{2}}, \lambda }}{T|{{\delta }_{2}}, {{\delta }_{1}}\Rightarrow T, {{q}_{1}}\wedge {{q}_{2}}, \lambda }. $

根据证明树, 可以得到缺省理论Γ的两个GD-扩展:${{E}_{1}}=Th(\{p, \neg {{q}_{1}}, {{q}_{2}}\}), {{E}_{2}}=Th(\{p, {{q}_{1}}\wedge {{q}_{2}}\}).$另一方面, 根据缺省理论扩展的定义, 缺省理论Γ有两个扩展:${{E}_{3}}=Th(\{p, \neg {{q}_{1}}\}), {{E}_{4}}=Th(\{p, {{q}_{1}}\wedge {{q}_{2}})\}, $且有${{E}_{3}}\subseteq {{E}_{1}}$E2=E4.

即缺省理论的扩展可能是其GD-扩展, 也可能是其GD-扩展的子集.

接下来, 我们考虑一个公式结构稍微复杂些的例子.

例4.3:给定缺省理论$\Gamma =(T, \Delta), T=\{p\}, \Delta =\{{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\}, $其中, ${{\delta }_{1}}=p\rightsquigarrow \neg {{q}_{1}}, $${{\delta }_{2}}=p\rightsquigarrow \neg {{q}_{3}}, $${{\delta }_{3}}=p\rightsquigarrow \neg {{q}_{4}}$以及${{\delta }_{4}}=p\rightsquigarrow (({{q}_{1}}\wedge {{q}_{2}})\wedge {{q}_{3}})\vee {{q}_{4}}.$

以序列L=δ1, δ2, δ3, δ4构造的证明树为例.

$ \frac{\frac{{{S}_{1}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}|{{\delta }_{4}}}\ \ \frac{{{S}_{2}}}{T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}|{{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}, \lambda }}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}}(\mathbf{TR}) $

首先分解左边的这一支S1, 可以得到

$ {{S}_{1}}=\frac{\frac{{{S}_{3}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}}\ \ \frac{{{S}_{4}}}{T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}|{{\delta }_{4}}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}|{{\delta }_{4}}}(\mathbf{TR}) $
$ {{S}_{3}}=\frac{\frac{{{S}_{5}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}|{{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}}\ \ \frac{{{S}_{6}}}{T, \neg {{q}_{1}}|{{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}}(\mathbf{TR}) $
$ {{S}_{4}}=\frac{T, \neg {{q}_{1}}, \neg {{q}_{3}}\vdash p\ \ T, \neg {{q}_{1}}, \neg {{q}_{3}}\not{\vdash }{{q}_{4}}}{T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}|{{\delta }_{4}}}(\mathbf{Atomi}{{\mathbf{c}}^{+}}) $
$ {{S}_{5}}=\frac{T\vdash p\ \ T\not{\vdash }{{q}_{1}}}{T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}|{{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}}(\mathbf{Atomi}{{\mathbf{c}}^{+}}) $
$ {{S}_{6}}=\frac{T, \neg {{q}_{1}}\vdash p, \ \ T, \neg {{q}_{1}}\not{\vdash }{{q}_{3}}}{T, \neg {{q}_{1}}|{{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}|{{\delta }_{3}}, {{\delta }_{4}}}(\mathbf{Atomi}{{\mathbf{c}}^{+}}) $

再来分解S2这一支, 可以得到(为了简化标记, 我们使用符号T' 表示集合$T\cup \{\neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}\}$):

$ {{S}_{2}}=\frac{\frac{{{S}_{7}}}{{T}'|p\rightsquigarrow ({{q}_{1}}\wedge {{q}_{2}})\wedge {{q}_{3}}\Rightarrow {T}', {{q}_{2}}}\ \ \frac{{{S}_{8}}}{{T}'|p\rightsquigarrow {{q}_{4}}\Rightarrow {T}', \lambda }}{{T}'|{{\delta }_{4}}\Rightarrow {T}', {{q}_{2}}}({{\vee }^{\uparrow }}) $
$ {{S}_{7}}=\frac{\frac{{{S}_{9}}}{{T}'|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}\Rightarrow {T}', {{q}_{2}}}\ \ \frac{{{S}_{10}}}{{T}'|p\rightsquigarrow {{q}_{3}}\Rightarrow {T}', \lambda }}{{T}'|p\rightsquigarrow ({{q}_{1}}\wedge {{q}_{2}})\wedge {{q}_{3}}\Rightarrow {T}', {{q}_{2}}}({{\wedge }^{\uparrow }}) $
$ {{S}_{8}}=\frac{{T}'\vdash p\ \ {T}'\vdash \neg {{q}_{4}}}{{T}'|p\rightsquigarrow {{q}_{4}}\Rightarrow {T}', \lambda }(\mathbf{Atomi}{{\mathbf{c}}^{+}}) $
$ {{S}_{9}}=\frac{\frac{{{S}_{11}}}{{T}'|p\rightsquigarrow {{q}_{1}}\Rightarrow {T}', \lambda }\ \ \frac{{{S}_{12}}}{{T}', \lambda |p\rightsquigarrow {{q}_{2}}\Rightarrow {T}'{{q}_{2}}}}{{T}'|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}\Rightarrow {T}', {{q}_{2}}}({{\wedge }^{\uparrow }}) $
$ {{S}_{10}}=\frac{{T}'\vdash p\ \ T\vdash \neg {{q}_{3}}}{{T}'|p\rightsquigarrow {{q}_{3}}\Rightarrow {T}', \lambda }(\mathbf{Atomi}{{\mathbf{c}}^{-}}) $
$ {{S}_{11}}=\frac{{T}'\vdash p\ \ T\vdash \neg {{q}_{1}}}{{T}'|p\rightsquigarrow {{q}_{1}}\Rightarrow {T}', \lambda }(\mathbf{Atomi}{{\mathbf{c}}^{-}}) $
$ {{S}_{12}}=\frac{{T}'\vdash p\ \ T\not{\vdash }\neg {{q}_{2}}}{{T}'|p\rightsquigarrow {{q}_{2}}\Rightarrow {T}', {{q}_{2}}}(\mathbf{Atomi}{{\mathbf{c}}^{+}}) $

节点S5, S6, S8, S10, S11S12的上层公式都是Atomic规则, 即它们都是叶子节点, 其他节点都是中间节点, 它们都是通过联结词的分解规则亦或是传递规则联结起来的.这样即构成了一棵以$T|{{\delta }_{1}}, {{\delta }_{2}}, {{\delta }_{3}}, {{\delta }_{4}}\Rightarrow T, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}, {{q}_{2}}$为根节点的证明树.

我们给出图 1证明树的结构示意图以帮助理解.

Fig. 1 Structure of proof tree 图 1 证明树结构示意图

根据证明树与GD-扩展的定义, 我们可以得到缺省理论Γ的一个GD-扩展${{E}_{1}}=Th(\{p, \neg {{q}_{1}}, \neg {{q}_{3}}, \neg {{q}_{4}}\}).$

类似地, 我们可以得到缺省理论Γ在其他23种序列下的证明树, 由于数目较多, 这里我们不再一一列举.从24种不同序列的证明树中, 我们可以根据定义得到缺省理论Γ的3个不同的GD-扩展.

$ \begin{array}{l} {E_1} = Th(\{ p, \neg {q_1}, \neg {q_3}, \neg {q_4}\} ), \\ {E_2} = Th(\{ p, \neg {q_1}, \neg {q_3}, (({q_1} \wedge {q_2}) \wedge {q_3}) \vee {q_4}\} ), \\ {E_3} = Th(\{ p, \neg {q_4}, ((({q_1} \wedge {q_2}) \wedge {q_3}) \vee {q_4}\} ). \end{array} $

根据缺省逻辑扩展的定义, E1, E2E3都是缺省理论Γ的扩展.即在这个缺省理论中, E1, E2E3既是缺省理论的扩展, 又是缺省理论的GD-扩展.并且, Γ任意的两个不同的GD-扩展的并集都是不协调的.

下面的例子则说明, 可能存在某些GD-扩展, 并不存在扩展, 使得这些GD-扩展与扩展之间有包含关系.

例4.4:给定缺省理论$\Gamma = (T, \Delta), T = \{ p\}, \Delta = \{ {\delta _1}, {\delta _2}, {\delta _3}\}, $其中, ${{\delta }_{1}}=p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}, $${{\delta }_{2}}=p\rightsquigarrow \neg {{q}_{1}}$以及${{\delta }_{3}}=p\rightsquigarrow \neg {{q}_{2}}.$

与例4.3类似, 可以得到缺省理论Γ在6种序列下的证明树, 因此下面的缺省矢列式都是GD-可证的.

$ \begin{array}{l} T|{\delta _1}, {\delta _2}, {\delta _3} \Rightarrow p, {q_1} \wedge {q_2}, \;\;\;T|{\delta _1}, {\delta _3}, {\delta _2} \Rightarrow p, {q_1} \wedge {q_2}, \;\;\;T|{\delta _2}, {\delta _1}, {\delta _3} \Rightarrow p, \neg {q_1}, {q_2}, \\ T|{\delta _2}, {\delta _3}, {\delta _1} \Rightarrow p, \neg {q_1}, \neg {q_2}, \;\;\;T|{\delta _3}, {\delta _1}, {\delta _2} \Rightarrow p, \neg {q_2}, {q_1}, \;\;\;T|{\delta _3}, {\delta _2}, {\delta _1} \Rightarrow p, \neg {q_2}, \neg {q_1}. \end{array} $

根据GD-扩展的定义, 我们可以得到缺省理论Γ的4种不同的GD-扩展.

$ \begin{array}{l} {E_1} = Th(\{ p, {q_1} \wedge {q_2}\} ), \;\;\;\;\;{E_2} = Th(\{ p, \neg {q_1}, {q_2}\} ), \\ {E_3} = Th(\{ p, \neg {q_1}, \neg {q_2}\} ), \;\;\;\;\;{E_4} = Th(\{ p, \neg {q_2}, {q_1}\} ). \end{array} $

根据缺省逻辑中扩展的定义, Γ的扩展为

$ {E_5} = Th(\{ p, {q_1} \wedge {q_2}\} ){\rm{和}}{E_6} = Th(\{ p, \neg {q_1}, \neg {q_2}\} ). $

从而有E1=E5, E3=E6, 即E1E3既是缺省理论的扩展, 又是缺省理论的GD-扩展.但是, 不同于例4.3, 在该例子中, GD-扩展E2E4并不包含该缺省理论的扩展.

那么贪婪缺省逻辑中缺省理论的GD-扩展是否也与扩展一样具有半单调性呢?我们先看下面的例子.

例4.5:给定缺省理论$\Gamma = (T, \Delta)$$\Gamma ' = (T, \Delta '), $$T = \{ p\}, \Delta = \{ {\delta _1}\}, \Delta ' = \{ {\delta _1}, {\delta _2}\}; $其中, ${{\delta }_{1}}=p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}, $${{\delta }_{2}}=p\rightsquigarrow \Subset \neg {{q}_{1}}.$

分别构造缺省理论ΓΓ' 的证明树.Γ只有1棵证明树如下:

$ \frac{\frac{p\vdash p\ \ p\not{\vdash }{{q}_{1}}}{p|p\rightsquigarrow {{q}_{1}}\Rightarrow p, {{q}_{1}}}\ \ \frac{p, {{q}_{1}}\vdash p\ \ p, {{q}_{1}}\not{\vdash }{{q}_{2}}}{p, {{q}_{1}}|p\rightsquigarrow {{q}_{2}}\Rightarrow p, {{q}_{1}}, {{q}_{2}}}}{p|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}\Rightarrow p, {{q}_{1}}\wedge {{q}_{2}}}. $

缺省理论Γ ' 有两棵证明树, 分别为

$ \frac{\frac{\frac{p\vdash p\ \ p\not{\vdash }{{q}_{1}}}{p|p\rightsquigarrow {{q}_{1}}, {{\delta }_{2}}\Rightarrow p, {{q}_{1}}|{{\delta }_{2}}}\ \ \frac{p, {{q}_{1}}\vdash p\ \ p, {{q}_{1}}\not{\vdash }{{q}_{2}}}{p, {{q}_{1}}|p\rightsquigarrow {{q}_{2}}, {{\delta }_{2}}\Rightarrow p, , {{q}_{1}}, {{q}_{2}}|{{\delta }_{2}}}}{p|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}, {{\delta }_{2}}\Rightarrow p, {{q}_{1}}\wedge {{q}_{2}}|{{\delta }_{2}}}\ \ \frac{p, {{q}_{1}}\vdash p\ \ p, {{q}_{1}}\vdash {{q}_{1}}}{p, {{q}_{1}}\wedge {{q}_{2}}|{{\delta }_{2}}\Rightarrow p, {{q}_{1}}\wedge {{q}_{2}}, \lambda }}{p|{{\delta }_{1}}, {{\delta }_{2}}\Rightarrow p, {{q}_{1}}\wedge {{q}_{2}}}, $
$ \frac{\frac{p\vdash p\ \ p\not{\vdash }{{q}_{1}}}{p|p\rightsquigarrow \neg {{q}_{1}}, {{\delta }_{2}}\Rightarrow p, \neg {{q}_{1}}|{{\delta }_{2}}}\ \ \frac{\frac{p, \neg {{q}_{1}}\vdash p\ \ p, \neg {{q}_{1}}\vdash \neg {{q}_{1}}}{p, \neg {{q}_{1}}|p\rightsquigarrow {{q}_{1}}\Rightarrow p, \neg {{q}_{1}}, \lambda }\ \ \frac{p, \neg {{q}_{1}}\vdash p\ \ p, \neg {{q}_{1}}\not{\vdash }\neg {{q}_{2}}}{p, \neg {{q}_{1}}|p\rightsquigarrow {{q}_{2}}\Rightarrow p, \neg {{q}_{1}}, {{q}_{2}}}}{p, \neg {{q}_{1}}|p\rightsquigarrow {{q}_{1}}\wedge {{q}_{2}}\Rightarrow p, \neg {{q}_{1}}, {{q}_{2}}}}{p|{{\delta }_{2}}, {{\delta }_{1}}\Rightarrow p, \neg {{q}_{1}}, {{q}_{2}}}. $

因此, 缺省理论Γ只有一个GD-扩展:$E=Th(\{p, {{q}_{1}}\wedge {{q}_{2}}\}), $缺省理论Γ' 有两个GD-扩展${{{E}'}_{1}}=Th(\{p, {{q}_{1}}\wedge {{q}_{2}}\})$${{{E}'}_{2}}=Th(\{p, \neg {{q}_{1}}, {{q}_{2}}\}), $其中, $E={{{E}'}_{1}}.$

根据上述的例子, 我们可以得到下面的定理.

定理4.6(GD-扩展的存在性). 一个缺省理论至少有一个GD-扩展.

定理4.7(GD-扩展的半单调性). 给定缺省理论Γ1=(T, Δ)和缺省理论Γ=(T, Δ' ), 满足D⊆ D' .如果E是缺省理论Γ1的一个GD-扩展, 那么一定存在缺省理论Γ2的一个GD-扩展E' ,使得EE' .

证明:因为E是缺省理论Γ1的一个GD-扩展, 根据GD-扩展的定义, 一定存在序列T1, T2, …, Ti, …(Ti的定义见定义2.12), 使得$E=Th\left(\bigcup\limits_{i=0}^{\infty }{{{T}_{i}}} \right).$下面我们证明存在E' ,使得EE' .

因为根据GD-扩展的定义, 对于每一个集合Ti, 都对应一个缺省规则δi+1, 并且δ1, δ2, …, δi, …是缺省规则集合Δ上的一个全序L.定义Δ=Δ' –Δ和Δ' 上的一个全序L' , L' 满足

● 对于任意δ1, δ2∈ Δ, 如果${{\delta }_{1}}{{\succcurlyeq }^{L}}{{\delta }_{2}}, $${{\delta }_{1}}{{\succcurlyeq }^{{{L}'}}}{{\delta }_{2}}; $

● 对于任意δ∈ Δ和δ' ∈ Δ, 都有$\delta {{\succcurlyeq }^{{{L}'}}}{\delta }'.$

因此根据定义, 按照序列L' 生成的GD-扩展E' 满足对于任意Ti, 都有TiE' .故而$Th\left(\bigcup\limits_{i=0}^{\infty }{{{T}_{i}}} \right)\subseteq {E}', $EE' .

定理4.8. 给定缺省理论Γ=(T, Δ), 如果存在公式的集合EΓ的扩展, 则存在Γ的一个GD-扩展E' ,使得EE.反之不成立.

证明:因为集合EΓ的扩展, 根据定理1.6, 存在一个集合的序列E0, …, Ei, …, 使得

$ E\_0=T;{{E}_{i+1}}=Th({{E}_{i}})\cup \{\psi |\phi \rightsquigarrow \psi \in \Delta, 其中, \phi \in {{T}_{i}}\text{ }并且\text{ }\neg \psi \not{\in }E\};E=\bigcup\limits_{i=0}^{\infty }{{{E}_{i}}}. $

故而, 令

$ \begin{align} & {{\Delta }_{0}}=\{\psi |\phi \rightsquigarrow \psi \in \Delta \text{, }QZ\text{, }\phi \in {{T}_{0}}\text{ }BQ\text{ }\neg \psi \not{\in }E\}; \\ & {{\Delta }_{i+1}}=\left\{ \psi |\phi \rightsquigarrow \psi \in \Delta-\bigcup\limits_{j=0}^{i}{{{\Delta }_{j}}}\text{, }QZ\text{, }\phi \in {{T}_{i}}\text{ }BQ\text{ }\neg \psi \not{\in }E \right\}, \\ \end{align} $

则有${E_{i + 1}} = Th({E_i}) \cup \{ \psi |\phi \psi \in {\Delta _i}\}.$并且, 对于每个${\Delta _i} = \{ {\delta _{i1}} = {\phi _{i1}}{\psi _{i1}}, {\delta _{i2}} = {\phi _{i2}}{\psi _{i2}}, ...\}, $都有:

$ \begin{array}{l} {E_i}|{\delta _{i1}}, {\delta _{i2}}, \cdots \Rightarrow {E_i}, {\psi _{i1}}|{\delta _{i2}}, {\delta _{i3}} \cdots \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \Rightarrow {E_i}, {\psi _{i1}}, {\psi _{i2}}|{\delta _{i3}}, {\delta _{i4}} \cdots \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \cdots \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \Rightarrow {E_i}, {\psi _{i1}}, \cdots {\psi _{ij}}|{\delta _{i(j + 1)}}, {\delta _{i(j + 2)}} \cdots \end{array} $

并且, $\{\psi |\phi \rightsquigarrow \psi \in {{\Delta }_{i}}\}=\bigcup\limits_{j=1}^{\infty }{\{{{\psi }_{ij}}\}}, $${{E}_{i+1}}=Th({{E}_{i}})\cup \bigcup\limits_{j=1}^{\infty }{\{{{\psi }_{ij}}\}}.$

我们将Δ中缺省规则的序列定义为$L::{{\delta }_{01}}, {{\delta }_{02}}, ...{{\delta }_{i1}}, {{\delta }_{i2}}, ...{{{\delta }'}_{1}}, ..., {{{\delta }'}_{i}}, ...$, 其中, ${{\delta }_{ij}}\in \bigcup\limits_{k=0}^{\infty }{{{\Delta }_{k}}}, {{\delta }_{{{i}'}}}\in \Delta -\bigcup\limits_{k=0}^{\infty }{{{\Delta }_{k}}}.$故而由L生成的序列E' 满足$E\subseteq {E}'.$

反之不成立, 见例4.4.在例4.4中, Th({p, q1q2})和Th({p, ¬ q1, ¬ q2})是Γ的GD-扩展, 又是Γ的扩展, 但是GD-扩展Th({p, ¬ q1, q2})和Th({p, ¬ q2, q1})都不是Γ的扩展.

我们可以得出贪婪缺省逻辑是不能退化为缺省逻辑的, 故而我们得到下面的定理.

定理4.9(不可退化性). 存在一个缺省理论Γ, 对于任意的集合E, 都有E是缺省理论Γ的扩展当且仅当E是缺省理论Γ的GD-扩展.

5 总结

本文提出了一种贪婪缺省逻辑, 旨在构造扩展时能尽可能地保留缺省规则中的信息, 并给出了贪婪缺省逻辑的推演系统—GD系统和贪婪缺省逻辑的GD-扩展的构造型定义.证明了贪婪缺省逻辑的存在性、半单调性和不可退化性等性质, 说明了贪婪缺省逻辑与经典缺省逻辑是两种不同的逻辑.

参考文献
[1] Reiter R. A logic for default reasoning.Artificial Intelligence, 1980, 13(1): 81–132. [doi:10.1016/0004-3702(80)90014-4]
[2] Antoniou G. A tutorial on default logics.ACM Computing Surveys (CSUR), 1999, 31(4): 337–359. [doi:10.1145/344588.344602]
[3] Etherington DW, Reiter R. On inheritance hierarchies with exceptions. In:Proc. of the AAAI. 1983, 83:104-108. https://vvvvw.aaai.org/Papers/AAAI/1983/AAAI83-017.pdf
[4] Hunter A. Using default logic in information retrieval. In:Proc. of the Symbolic and Quantitative Approaches to Reasoning and Uncertainty. 1995. 235-242.[doi:10.1007/3-540-60112-0_27]
[5] Brewka G. Nonmonotonic Reasoning:Logical Foundations of Commonsense. Vol.12, Cambridge University Press, 1991.
[6] Lukaszewlcz W. Two results on default logic. In:Proc. of the 9th Int'l Joint Conf. on Artificial Intelligence, Vol.1. Morgan Kaufmann Publishers Inc., 1985. 459-461. http://dl.acm.org/citation.cfm?id=1625225
[7] Baader F, Hollunder B. Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic.Journal of Automated Reasoning, 1995, 15(1): 41–68. [doi:10.1007/BF00881830]
[8] Schaub T. On constrained default theories. In:Proc. of the ECAI. 1992. 304-308. http://www.intellektik.informatik.tu-darmstadt.de/TR/1992/92-02.ps.Z
[9] Mikitiuk A, Truszczynski M. Constrained and rational default logics. In:Proc. of the IJCAI. 1995. 1509-1517. http://ijcai.org/Proceedings/95-2/Papers/064.pdf
[10] Cholewinski P, Marek VW, Truszczynski M. Default reasoning system deres.KR, 1996, 96: 518–528.
[11] Baader F, Hollunder B. Embedding defaults into terminological knowledge representation formalisms.Journal of Automated Reasoning, 1995, 14(1): 149–180. [doi:10.1007/BF00883932]
[12] Kolovski V, Parsia B, Katz Y. Implementing owl defaults. Technical Report, DTIC Document, 2006.
[13] Zang L, Cao C, Sui Y. Two-Level default theories. In:Proc. of the Int'l Conf. on Artificial Intelligence (ICAI), p.1, The Steering Committee of the World Congress in Computer Science, Computer Engineering and Applied Computing (WorldComp). 2013. http://search.proquest.com/openview/a93eb9dda9bb0a7ddef38039f5b2485a/1?pq-origsite=gscholar&cbl=1976349
[14] Zang L, Wang W, Chen B, Cao C. The double-level default description logic mathcal d3l. In:Knowledge Science, Engineering and Management. 2015. 141-146.[doi:10.1007/978-3-319-25159-2_12]
[15] Takeuti G. Proof Theory. 2nd ed., Courier Corporation, 2013.