core.logic 占主导地位的竞技场 [软]答案

【问题标题】：Arenas where core.logic dominates [soft]core.logic 占主导地位的竞技场 [软]
【发布时间】：2012-06-07 05:01:33
【问题描述】：

社区维基

我不在乎声望点，我只想要好的答案。随时将此问题标记为社区 wiki。

上下文

我一直在研究 The Reasoned Schemer，并发现了以下观察结果：

逻辑编程很有意思。
逻辑编程有时是违反直觉的
逻辑编程通常是“低效的”（或者至少是我编写的代码）。

好像是从
汇编 -> C++，我“放弃”了编写自己的机器代码的控制权
C++ -> Clojure，我放弃了对内存管理的控制
Clojure -> core.logic/prolog/minikanren，我失去了对如何完成计算的部分控制

问题：

除了 (1) 解决逻辑难题和 (2) 类型推断之外，逻辑编程主导的问题领域有哪些？

谢谢！

【问题讨论】：

这似乎与之前在这里提出的其他问题有关：real-world applications of prolog 和 real-world prolog usage。（请注意问题是如何结束的）。

标签： clojure prolog logic minikanren

【解决方案1】：

Constraint logic programming 对于解决各种调度、资源分配和其他重要的约束满足/组合优化问题非常有用。您所拥有的只是声明性的：约束（例如，一次只能有一架飞机在跑道上），也许您想要最小化/最大化（吞吐量/等待）。

Prolog 中有各种众所周知的风格，包括在有限整数域中工作的CLP(FD)，以及在实数域中工作的 CLP(R)。至少 CLP(FD) 似乎在core.logic's immediate roadmap 中。

我相信这种源自 Prolog 的解决方案正积极用于air traffic control 和其他物流任务，尽管很难获得准确的信息，这些对任务和生命至关重要的公司到底在使用哪些技术。

【讨论】：

【解决方案2】：

人工智能研究，特别是认知机器人技术和基于逻辑的知识表示的其他应用，是 Prolog 被大量使用的领域，因为它与逻辑理论密切相关。这种关系非常有用，因为它基本上将理论带入了生活。定理可以在纸上证明，然后在 prolog 中几乎可以轻松地实现并执行，并且执行的程序具有证明的属性。这允许程序“通过构造正确”，这与首先编写程序然后尝试证明它们的属性相反（就像在正式方法中所做的那样，使用例如模型检查）。

语义网是逻辑编程发挥越来越大作用的另一个地方。

【讨论】：

我相信人工智能和机器人技术，概率方法（可以处理噪声）主导基于逻辑的方法（不能处理噪声）。
@user1311390 用于不同目的的不同人工智能分支；概率方法当然不适合做一些事情。
当然还有关于概率逻辑的研究：例如见MCMC
@user1311390 - 在 cognitive 机器人技术中，逻辑编程被大量使用，因为它经常被用作基于形式推理的认知理论的测试平台。一些反应式机器人系统（基于 Brooks 的包容架构）植根于形式逻辑。最后，计算语言学深深植根于形式系统，定理（和语法）证明器非常适合逻辑编程。