逻辑编程和自动定理证明的区别

Question

逻辑编程和自动定理证明（ATP）（如E-Prover、Spass或Princess）有什么区别？

我搜索了很多资料，唯一找到的信息是ATP是逻辑编程的前身。但我并不看出两者之间的区别。但我猜想它应该不止于语法上的差异。

- 2Application

---

这篇论文有助于说明差异：在逻辑编程中实现定理证明器。 - lurker

Answer 1

就Prolog部分而言，Richard O'Keefe说得最好：

Prolog是一种高效的编程语言，因为它是一个愚蠢的定理证明器。

因此，Prolog和定理证明之间存在联系。Prolog具有某些定理证明器的特征，例如，它搜索证明或者更确切地说是消解反驳，但它以一种不完全的方式进行搜索，这种方式更适合于一般用途的编程语言。

当然，Prolog和定理证明器之间的相似性使Prolog成为实现更完整的定理证明器的绝佳选择。

事实上，相对容易增强和扩展Prolog的不完整默认执行策略，使搜索变得更加完整。

请注意，Prolog还表现出一些超逻辑特征，超出了定理证明的范围，实际上通常会妨碍声明式推理。另请参见logical-purity。

- mat

---

这里的“不完整”一词需要一些说明：仅当Prolog陷入无限循环或其他错误时，它才是不完整的。 - false

我觉得应该把“another”这个限定词去掉，您的看法呢？ - mat

啊，应该更好地解释一下“错误”的含义。这是指一些被标记的异常。 - false

@mat，你有引用的参考资料吗？ - S0rin