ASP中的基本概念

析取逻辑与传统逻辑程序

一个一阶逻辑的语句，经过Skolem化后可以等价转化为子句：

$${\mathrm{\forall }}_{x_1}\dots {\mathrm{\forall }}_{x_s}(L_1\vee \cdots \vee L_m)$$

复习一下一阶逻辑，有

$$A\leftarrow B\iff A\vee \mathrm{\neg }B$$

那么对于刚好含有一个正文字的子句（确定子句），就可以写成以条件运算符表示的规则形式：

$$A\leftarrow B_1,\dots ,B_n.$$

它是${\mathrm{\forall }}_{x_1}\dots {\mathrm{\forall }}_{x_s}(A\vee \mathrm{\neg }(B_1\wedge \cdots \wedge B_n))$的等价形式。 确定子句的有限集合称为 （传统）逻辑程序。

任给一个逻辑程序$P$，$P$中所有常项的集合称为$P$的Herbrand域$U(P)$。 一阶逻辑的一个解释$I$由一个论域$D$，和一个从项和公式到$D$上函数和关系的映射$V$构成。 而一个传统逻辑程序$P$的一个Herbrand解释$I_H(P)$是一个三元组$⟨U(P),V_H,M(P)⟩$。 其中，论域就是$P$的Herbrand域，映射$V_H$把任何常项和常原子映射为其自身。 因此对于一个确定的$P$，$U(P)$和$V_H$都是确定的。 $M(P)$是一个“指派”集合，是$P$中所有常原子集合（Herbrand基）$B(P)$的子集。 任何常原子$p$在指派$M(P)$下为真，当且仅当$p\in M(P)$。 一个Herbrand解释称为一个程序的Herbrand模型，如果该程序的所有规则在该解释下为真。Herbrand模型具有以下性质：

• 任意子句集，如果存在一阶模型，则必然存在Herbrand模型。
• 任何传统逻辑程序有Herbrand模型。
• 任何传统逻辑程序的任意两个Herbrand模型的交是该程序的一个Herbrand模型。
• 任何传统逻辑程序$P$有唯一的最小Herbrand模型$\mathrm{\Gamma }(P)$。
• 给定传统逻辑程序$P1$, $P2$，如果$P1\subseteq P2$，则$\mathrm{\Gamma }(P1)\subseteq \mathrm{\Gamma }(P2)$。

失败即否定与非单调推理

传统逻辑程序只能推理正文字形式的结论。 为了推理含有负文字的逻辑程序，需要增加额外的规则。 “失败即否定（negation as failure, NAF）”就是这样的一个规则，即：如果常原子$A$无法被推出，则推出$\mathrm{not}A$。

经典的一阶逻辑是单调的，即：如果语句$A$是语句集$T$的逻辑结论，那么一定是$T$的任意超集的结论。 说人话就是，新规则的加入不影响已有结论的成立。 在NAF规则下进行的推理是非单调的，增加新知识后原有结论可能不再成立。例如：

• 鸟会飞，Tweety是鸟 $\to$ Tweety会飞
• 鸟会飞，Tweety是鸟，Tweety不会飞 $\to$ Tweety不会飞
• 鸟会飞，企鹅不会飞，Tweety是鸟，Tweety是企鹅 $\to$ Tweety不知是否会飞
• 企鹅是鸟，鸟会飞，企鹅不会飞，Tweety是鸟，Tweety是企鹅 $\to$ Tweety不会飞