SLD Resolution生成子句是否为P的逻辑推论及Herbrand集相关问题

首先直接给结论：不是所有生成的子句都是程序P的逻辑推论——准确来说，SLD消解过程中产生的每个目标子句，是初始目标子句与P共同的逻辑推论，而非单独P的逻辑推论。但如果我们的推导最终得到了空子句（也就是“推导成功”），那反过来能证明初始目标的否定是P的逻辑推论。

为什么这么说？得从SLD消解的步骤和逻辑含义拆解：

• 程序P是由确定Horn子句组成的，每个子句形如B ← B₁,B₂,...,Bₖ，逻辑上等价于B₁∧B₂∧...∧Bₖ → B（如果所有Bᵢ都为真，那B一定为真）。
• 目标子句形如← A₁,A₂,...,Aₙ，逻辑上等价于¬(A₁∧A₂∧...∧Aₙ)（我们要证明的是这个命题是否能被P“反驳”）。

SLD消解的每一步，都是拿当前目标子句里的某个文字Aᵢ，和P里的某个子句B ← B₁...Bₖ做合一（找到置换θ让Aᵢθ=Bθ），然后生成新的目标子句← (A₁,...,Aᵢ₋₁,B₁,...,Bₖ,Aᵢ₊₁,...,Aₙ)θ。

从逻辑推导的角度看：如果我们假设初始目标←A₁...Aₙ是真的（也就是A₁∧...∧Aₙ是假的），再结合P中的子句B←B₁...Bₖ，那么新目标子句一定也是真的。换句话说，P ∪ {初始目标} ⊨ 新目标子句——这是每一步消解都保证的。但单独看P的话，新目标子句不一定是P的逻辑推论，因为初始目标本身可能不是P的推论（毕竟我们就是要通过推导来验证初始目标是否和P矛盾）。

你这里可能混淆了几个概念，先理清楚：

首先，最小Herbrand模型Mₚ是程序P的所有Herbrand模型的交集——简单说，就是所有能被P“必然证明”的基原子（不含变量的原子命题）的集合。如果一个基原子Q在Mₚ里，就意味着P的任何模型都满足Q，也就是P⊨Q。

然后，当我们用目标子句←Q（Q是基原子）启动SLD推导，**推导成功（得到空子句）**意味着什么？这说明P∪{←Q}是不可满足的——也就是不存在任何模型同时满足P和←Q（即¬Q）。反过来就是说，所有满足P的模型都必须满足Q，也就是P⊨Q，那Q自然属于最小Herbrand模型Mₚ。

那为什么推导成功就能确定Q在最小Herbrand模型里？这是SLD消解的完备性保证的：如果Q属于Mₚ（也就是P⊨Q），那么一定存在从←Q出发的SLD反驳（推导成功）；反过来，如果存在这样的反驳，那么P⊨Q，Q一定在Mₚ里。

回到你的疑问：“若每个目标子句都是P的逻辑推论，为何推导成功就能确定其属于最小Herbrand集？”其实这里的关键点是，推导成功时，我们得到的结论不是目标子句属于Herbrand集，而是目标子句的否定（也就是Q）属于最小Herbrand模型。因为目标子句←Q等价于¬Q，推导成功说明P和¬Q不能同时成立，所以P必须蕴涵Q，而Q作为基原子，就必然在最小Herbrand模型里——毕竟最小Herbrand模型就是所有P必然蕴涵的基原子的集合。

内容的提问来源于stack exchange，提问作者Qwerto