我正在观察一些问题,例如Logica模糊逻辑和Horn子句,并看到了一些简单的应用程序示例,使用Prolog.
这个问题的原因是因为这些问题也属于Herbrand定理,我认为它比其他定理要复杂一些,至少对我而言,我很难找到与Prolog相关的应用示例.
这就是为什么我想用Prolog提供一些应用实例,而不是那么基本(因为根据定义生成Herbrand模型,是基本规则,并且总是在搜索Herbrand时找到这个应用程序示例),专供Herbrand使用.谢谢
这是Prolog中的示例应用代码:
p(f(X)):- q(g(X)).
p(f(X)):- p(X).
p(a).
q(b).
一组子句有一个模型,当且仅当它有一个Herbrand模型.
为了证明该条款C是条款的结果Cs,只需表明Cs∪ ~C是不可满足的.
从抽象的角度来看,这是Prolog所做的,通过一个特殊的解决方案:你可以将执行一个(纯粹的 - 其他)Prolog程序看作Prolog引擎试图找到否定查询的解析反驳.
Prolog实施的解决方案形式,SLD解决方案 采用深度优先搜索,并不能保证所有不可满足的条款都被反驳,但 不完整.
在Prolog中,程序属性可能会影响后果的推导.例如,使用您的程序:
?- p(X). wating...
而我们只是将条款重新排序为:
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.