人工智能哲学
PROLOG(Clocksin and Mellish 1981)的“以否定为失败”的思想形式化。通过引入推理规则：“根据前提p和不能推断出9，推断出r”，对普通逻辑加以扩展。其思想是，在缺乏特定的压倒一切的信息q的情况下，r是根据p得到的有缺省的结论。我们看一个例子
$$
( \mathbf { a } ) \# \mathbb { H } \gnapprox ( \exists \models ( \square \rtimes ) )
$$
(a能飞)
这里，“相容算式”表示该算式与系统中所有的推理都是相容的。这样，对于任何给定的鸟，我们就可以按正常情况推断出它能飞，但是如果存在着用于推导出反常情况的公理，就可以以它们为“门”，把这一规则拒之门外。与这种形式大体相似的系统已由赖特(Reiter1980))，麦克德莫特和多伊尔(McDermott and Doyle 1980))，克拉克(Clark1978)，以及其他人作过研究。
划界法是由麦卡锡(McCarthy1980)和他的同事(Lifschitz1985;Lifschitz未刊稿")发明的，它避免了增加新的推理规则，而主张采用一个带有公理的一阶理论，以表达使某一谓词“极小化”的目标。举例说，现有公理
(对所有(x)(如果(与(鸟 x)(非(反常x)))(x能飞)))
若能使反常谓词极小化，就可以像以前那样，对每一个给定的鸟，按正常方式推断出它是能飞的。为了实现这一点，就要在原有理论中增加一个二阶公理。设A(反常；鸟)是已有的全部公理的合取。(最好是有限的。)我们在A后的括号里写出想要替换的谓词的名称。分号把准备被极小化的谓词(反常)与“变量”谓词(鸟)分开；通常可能有一个或多个谓词要被极小化，有零个或多个变量。所以A(foo;baz)可作为同一公理集，其中foo代替反常，baz代替鸟。根据这种标记法，新的公
[1] V.利夫席茨(Lifschitz 1986)，“点式划界法”，未出版手稿，1986 年1月 16日。
234