2Ap*_*ion 6 prolog logic-programming theorem-proving
逻辑编程和自动定理证明(ATP)之间有什么区别(例如使用E-Prover,Spass或Princess)？
我搜索了很多,我发现的唯一信息是ATP是逻辑编程的先驱.但我没有看到差异.但我想这不仅仅是语法.
mat*_*mat 10
就问题的Prolog部分而言,Richard O'Keefe最好说:
Prolog是一种高效的编程语言,因为它是一个愚蠢的定理证明者.
因此,Prolog和定理证明之间存在联系.Prolog具有定理证明器的一些特征,例如,它搜索证明或更确切地说是解析反驳,但它以不完整的方式执行,更适合于通用编程语言.
当然,Prolog和定理证明器之间相对紧密的亲和力使Prolog成为实现更成熟的定理证明器的绝佳选择.
事实上,增加和扩展Prolog的不完整默认执行策略相对容易,以便搜索变得更加完整.
请注意,Prolog还展示了一些超出定理证明范围的超逻辑特征,实际上通常会妨碍声明性推理.另见逻辑纯度.