Prolog中的Herbrand

Question

我正在关注一些与模糊逻辑和Horn子句相关的问题，并看到了一些简单的应用示例，使用Prolog。

我提出这个问题的原因是因为这些问题也属于Herbrand定理，我认为这比其他问题更加复杂，至少对我来说是这样的，而且我很难找到一个与Prolog相关的应用示例。

因此，我希望提供一些使用Prolog的应用示例，不要太基础（因为根据定义生成Herbrand模型的是基本规则，并且在搜索Herbrand时总是会找到这个应用示例），专门用于Herbrand。谢谢。

以下是Prolog中的一个应用示例代码：

p(f(X)):- q(g(X)).
p(f(X)):- p(X).
p(a).
q(b).

- Jonatan Lavado

Answer 1

一组子句有模型当且仅当它有Herbrand模型。

要证明子句C是子句Cs的结果，只需证明Cs∪~C是不可满足的。

这就是Prolog所做的抽象术语，通过特殊情况的resolution：你可以把一个（纯粹的——还有什么）Prolog程序的执行看作是Prolog引擎试图找到否定查询的resolution反驳。

Prolog实现的resolution形式，SLD resolution with depth-first search，并不保证所有不可满足的子句都被证明为错误的，它是不完整的。

在Prolog中，过程属性可能会影响推导结果。例如，使用以下程序：

?- p(X). 等待...

而我们只需要重新排列子句：

q(b). p(a). p(f(X)):- q(g(X)). p(f(X)):- p(X).

我们得到：

?- p(X).
X = a ;
X = f(a) ;
X = f(f(a)) .

请注意，许多重要的声明性属性确实在Prolog的纯净和单调子集中得到了保留。有关更多信息，请参见 logical-purity。

- mat