缺省逻辑是 Ray Reiter 提出的用来形式化有缺省假定的推理的非单调逻辑。 缺省逻辑可以表达像“缺省的，某个事物是真的”的事实；相反的，标准逻辑只能表达某个事物为真或某个事物为假。这是一个问题，因为推理经常涉及在多数时候是真但不总是真的事实的推理。经典的例子是: “鸟通常会飞”。这个规则可以在标准逻辑中表达为要么“所有鸟都会飞”，这与企鹅不会飞的事实相矛盾；要么“除了企鹅、鸵鸟 ... 的所有鸟都会飞”，这要求规则指定出所有的例外。缺省逻辑致力于形式化像这样的推理规则，而不需要明确提及所有的例外。

语法

例子

限制

语义

蕴涵(怀疑的 轻信的 正当的 简明的 约束的 合理的 谨慎的)

断言变体

语法

缺省理论是 <math>\\langle D, W \\rangle</math> 对。<math>W</math> 是逻辑公式的集合，叫做背景理论，形式化的是确实已知的事实。<math>D</math> 是缺省规则的集合，每个都有形式:

<math>\\frac{Prerequisite : Justification_1, ..., Justification_n}{Conclusion}</math>

依据这种缺省，如果我们相信 <math>Prerequisite</math>(先决条件)是真的，并且每个 <math>Justification_i</math>(论据)都相容于我们当前的信仰，我们导出信仰 <math>Conclusion</math>(结论)是真的。

在 <math>W</math> 中逻辑公式和在缺省中的所有公被初始的假定为一阶逻辑公式，但是它们潜在的可以是任意形式逻辑的公式。公式都是命题逻辑的情况是研究最多的。

例子

缺省规则 “鸟通常会飞” 被下列缺省所形式化:

<math>D = \\left\\{ \\frac{Bird(X) : Flies(X)}{Flies(X)} \\right\\}</math>

这个规则意味着，如果 <math>X</math> 是鸟，并且可以假定它会飞，则我们得出结论它会飞。包含某些关于鸟的事实的背景理论在下面列出:

W = { Bird(秃鹫), Bird(企鹅), &not; Flies(企鹅), Flies(鹰) }。

依据这个缺省规则，秃鹫会飞，因为前件 Bird(秃鹫) 是真的，并且论据 Flies(秃鹫) 与当前已知不矛盾。相反的，Bird(企鹅) 不允许得出结论 Flies(企鹅): 即使缺省的前件 Bird(企鹅) 是真的，论据 Flies(企鹅) 与已知相矛盾。从这个背景理论和这个缺省，不能得出结论 Bird(鹰)，因为缺省规则只允许从 Bird(X) 推出 Flies(X)，但不能反过来。从推论规则的结论推出前提是结论的一种解释形式，这是溯因推理的目标。

常见的缺省假定是不知道为真的东西都被相信是假的。这叫做封闭世界假定，并在缺省逻辑中对每个事实 <math>F</math> 使用像下列这样的缺省来形式化。

<math>\\frac{:{\eg}F}{{\eg}F}</math>

例如，计算机语言 Prolog 在推导否定的时候，使用了某种程度的缺省假定: 如果否定的原子不能被证明为真，则它被假定为假。但是要注意，Prolog 使用了所谓的否定为失败: 当解释器必须求值原子 <math>\eg F</math> 的时候，它尝试证明 <math>F</math> 是真，并如果这失败了则结论为 <math>\eg F</math> 是真。转而在缺省逻辑中，缺省有 <math>\eg F</math> 作为论据，它只能在 <math>\eg F</math> 与当前知识一致的时候应用。

限制

缺省是无条件的或无先决条件的，如果它没有先决条件(或者等价的说先决条件是重言式)。一个缺省是正规的，如果它有等价于它的结论的一个单一论据。一个缺省是超正规的，如果它是无条件的和正规的。一个缺省是半正规的，如果它的所有论据都蕴涵它的结论。一个缺省理论叫做无条件的、正规的、超正规的、或半正规的，如果它包含的所有缺省分别都是无条件的、正规的、超正规的或半正规的。

语义

一个缺省规则可以应用于一个理论，如果它的前件被这个理论所蕴涵，并且它的论据都一致于这个理论。缺省规则的应用导致它的结论增加到这个理论。其他缺省规则接着可以应用于结果的理论。当没有缺省规则可以应用于理论的时候，这个理论就叫做缺省理论的扩展。缺省规则可以按不同的次序应用，这可以导致不同的扩展。尼克松菱形例子是有两个扩展的缺省理论:

<math>

\\left\\langle \\left\\{ \\frac{Republican(X):\eg Pacifist(X)}{\eg Pacifist(X)}, \\frac{Quaker(X):Pacifist(X)}{Pacifist(X)} \\right\\}, \\left\\{Republican(Nixon), Quaker(Nixon)\\right\\} \\right\\rangle </math>

因为 尼克松既是共和党的人又是教友会的人，两个缺省都可以应用。但是，应用第一个缺省导致尼克松是不爱好和平的人的结论。以同样的方式，应用第二个缺省我们得出尼克松是爱好和平的人，因此使第一个缺省不可应用。这种特定的缺省理论因此有两个扩展，其中一个 <math>Pacifist(Nixon)</math> 是真，而另一个 <math>Pacifist(Nixon)</math> 是假。

缺省逻辑的最初的语义基于的是函数的不动点。下面是一个等价的算法定义。如果缺省包含有自由变量的公式，它被认为表示通过向所有这些变量给出一个值而得到所有缺省的集合。缺省 <math>\\frac{\\alpha:\\beta_1,\\ldots,\\beta_n}{\\gamma}</math> 对命题理论 <math>T</math> 是可应用的，如果 <math>T \\models \\alpha</math> 并且所有理论 <math>T \\cup \\{\\beta_i\\}</math> 是一致的。这个缺省对 <math>T</math> 的应用得到理论 <math>T \\cup \\{\\gamma\\}</math>。通过应用下列算法可以生成一个扩展:

T=W /* 当前理论 */

A=0 /* 迄今应用的缺省的集合 */

/* 应用一序列的缺省 */

while 有个不在 A 中的缺省 d 对于 T 是可应用的

增加 d 的结论到 T

增加 d 到 A

/* 最终的一致性检查 */

if

for 所有缺省 d in A

T 一致于 d 的所有论据

then

输出 T

这个算法是非确定性的，因为对于给定的理论 <math>T</math> 有很多缺省可以应用。在尼克松菱形的例子中，第一个缺省的应用导致第二个缺省不能应用的一个理论，反之亦然。作为结果，可以生成两个扩展: 在其中一个里尼克松是爱好和平的人和另一个里尼克松不爱好和平的人。

最终的所有已经应用的缺省的论据的一致性检查使某些理论不能有任何扩展。特别是，这发生在对于可应用的缺省的所有序列这个检查都失败的时候。下列缺省理论就没有扩展:

<math>

\\left\\langle \\left\\{ \\frac{:A(b)}{\eg A(b)} \\right\\}, \\emptyset \\right\\rangle </math>

因为 <math>A(b)</math> 一致于缺省被应用到的背景理论，所以得出结论 <math>A(b)</math> 是假的。但是这个结果破坏了应用第一个缺省所有做的假定。因此，这个理论没有扩展。

正规的缺省理论保证至少有一个扩展。进一步的，正规缺省理论的扩展是相互矛盾的。

蕴涵

缺省理论可以有零个、一个或更多的扩展。从一个缺省理论到一个公式的蕴涵可以用两种方式定义:

怀疑的

一个公式被一个缺省理论所蕴涵，如果它被它的所有扩展所蕴涵；

轻信的

一个公式被一个缺省理论所蕴涵，如果它被它的至少一个扩展所蕴涵；

例如，尼克松菱形例子有两个扩展，在其一中尼克松是爱好和平的人在另一个中他不是爱好和平的人。因此，Pacifist(尼克松) 和 &not; Pacifist(尼克松) 都不被怀疑的蕴涵，而二者都被轻信的蕴涵。如这个例子展示的，缺省理论的轻信结论可以相互矛盾。

可供选择的语义

缺省逻辑下列可供选择的语义都是基于同最初一样的语法。

正当的

同最初的语义不同之处是，如果缺省使集合 <math>T</math> 矛盾于已应用的缺省的一个论据，则不应用这个缺省；

简明的

只在缺省的结论没有被 <math>T</math> 所蕴涵的时候应用它(精确的定义更加复杂，这只是背后的想法)；

约束的

只在背景理论和所有应用的(包括这个)缺省的论据和结论所构成集合是一致的时候应用它；

合理的

类似于约束的缺省逻辑，但是在一致性检查中不考虑缺省的结论；

谨慎的

缺省可以应用但相互冲突(像尼克松菱形的例子)的不应用。

正当的和约束的语义为所有的缺省理论指派至少一个扩展。

缺省逻辑的变体

缺省逻辑的下列变体同最初的语法和语义二者有所区别。

断言变体

断言是由一个公式和一个公式的集合构成的 <math>\\langle p: \\{r_1,\\ldots,r_n\\} \\rangle</math> 对。这种对指示 <math>p</math> 是真，当公式 <math>r_1,\\ldots,r_n</math> 已经被假定为一致于证明 <math>p</math> 为真的时候。一个断言缺省理论由叫做背景理论的断言理论(断言公式的集合)和按原始语法定义的缺省的集合构成。当一个缺省应用于断言理论的时候，把由它的结论和它的论据合成的对增加到这个理论。下列语义使用了断言理论:

积累缺省逻辑

委托假定缺省逻辑

准缺省逻辑

弱扩展

不再检查前件在由背景理论和已应用的缺省的结论构成的理论中是否是有效的，检查前件在将要生成的扩展中的有效性；换句话说，生成扩展的算法开始于猜测一个理论并使用它代替背景理论；从扩展生成的过程得到的结果实际上是一个扩展，只在它等价于在开始时所猜测的理论的时候。缺省逻辑的这个变体在原理上与自动认识逻辑有关，在那里理论 <math>\\Box x \\rightarrow x</math> 有一种模型，在其中 <math>x</math> 是真，只是因为假定 <math>\\Box x</math> 为真，公式 <math>\\Box x \\rightarrow x</math> 支持这个初始假定。

析取缺省逻辑

缺省的结论是公式的集合而不是单一的公式。在应用缺省的时候，至少其中一个结论被非确定性的选择为真。

缺省上的优先级

可以明确的指定缺省的相对优先级；在可以应用于一个理论的缺省之间，只有最高优先级的可以应用。缺省逻辑的某些语义不要求明确指定优先级；而是更多特殊性(在更少情况下可应用的)缺省优于更少特殊性的缺省。

统计变体

统计缺省对缺省附加错误频率的上限；换句话说，缺省被假定为是不正确的推理规则，应用它的次数到了这个分数的时候。

转换

缺省理论可以被转换成其他逻辑的理论或反之。转换要考虑下列条件:

结论保持

最初和转换后的理论有同样的(命题)结论；

忠实

这个条件有意义只在如下转换的时候，在缺省逻辑的两个变体之间、或在缺省逻辑和在其中类似于扩展的概念比如模态逻辑中模型存在的逻辑之间；一个转换是忠实的，如果在最初和转换后的理论的扩展(或模型)之间存在一个映射(典型的是双射)；

模块化

从缺省逻辑到其他逻辑的转换是模块化的，如果缺省和背景理论可以分开转换；此外，向北京理论增加公式只导致向转换的结果增加新公式；

同字母表

最初和转换后的理论建立在相同的字母表之上；

多项式

转换的运行时间和生成的理论的大小要求是最初理论的多项式。

转换典型的要求忠实或至少是结论保持，而模块化和同字母表的条件有时被忽略。

在命题缺省逻辑和下列逻辑之间的转换已经研究过了:

经典命题逻辑；

自动认识逻辑；

限定于被正规理论的命题缺省逻辑；

缺省逻辑的可作为替代的语义；

界限。

转换存在与否依赖于施加那种条件。从命题缺省逻辑到经典命题逻辑的转换不能总是生成多项式大小的命题理论，除非多项式层次瓦解。到自动认识逻辑的转换存在与否依赖于是否要求模块性或使用相同的字母表。

复杂性

关于缺省逻辑的下列问题的计算复杂性是已知的:

扩展的存在性

决定一个命题缺省理论是否有至少一个扩展是 <math>NP^{NP}</math>-完全的；

怀疑的蕴涵

决定一个命题缺省理论是否怀疑的蕴涵一个命题公式是 <math>co-NP^{NP}</math>-完全的；

轻信的蕴涵

决定一个命题缺省理论是否轻信的蕴涵一个命题公式是 <math>NP^{NP}</math>-完全的；

扩展检查

决定一个命题公式是否等价于一个命题缺省理论的扩展是 <math>P^{NP[log]}</math>-完全的；

模型检查

决定一个命题释义是否是一个命题缺省理论的扩展的模型是 <math>NP^{NP}</math>-完全的。

实现

有两个系统实现了缺省逻辑：DeReS 和XRay。