gpt4 book ai didi

prolog - 逻辑编程和自动定理证明之间的区别

转载 作者:行者123 更新时间:2023-12-04 13:58:35 24 4
gpt4 key购买 nike

逻辑编程和自动定理证明 (ATP)(例如使用 E-Prover、Spass 或 Princess)有什么区别?

我搜索了很多,我发现的唯一信息是 ATP 是逻辑编程的先驱。但我看不出有什么区别。但我想这不仅仅是语法。

最佳答案

就问题的序言部分而言,理查德·奥基夫 (Richard O'Keefe) 说得最好:

Prolog is an efficient programming language because it is a stupid theorem prover.



因此,序言和定理证明之间存在联系。 Prolog 具有定理证明器的一些特征,例如,它搜索 。样张或者更确切地说 决议反驳 ,但它在 中这样做不完整 更适合通用编程语言的方式。

当然,Prolog 和定理证明者之间比较接近的亲和力使得 Prolog 成为 的绝佳选择。实现 更成熟的定理证明者。

实际上,对Prolog的不完全默认执行策略进行扩充和扩展,从而使搜索变得更加完整是比较容易的。

但请注意,Prolog 还展示了一些超出定理证明范围的逻辑外特征,实际上通常会妨碍声明式推理。另见 .

关于prolog - 逻辑编程和自动定理证明之间的区别,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36335633/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com