将一阶逻辑转换为 CNF答案

【问题标题】：Convert First-Order Logic to CNF将一阶逻辑转换为 CNF
【发布时间】：2011-08-31 20:26:19
【问题描述】：

我正在努力使用MiniSat 来解决约束满足问题。在一阶逻辑中，问题很容易用一些离散域变量和一些谓词来表示。

但是，MiniSat 以及我目前看到的其他 CSP 求解器都希望他们以 CNF 形式输入。所以我正在寻找一种可以将一阶逻辑表达式转换为 CNF 的“预处理器”。

有什么想法吗？

【问题讨论】：

如果我误解了你的问题，我很抱歉，但我想知道 CNF 是否对一阶逻辑有足够的表达能力。例如“任何人（X）的父亲的兄弟是他（X）的叔叔”可以简单地翻译为一阶逻辑。但是（就我所记得的从句而言）在我看来，从句无法表达这种普遍性（更准确地说，是“任何人”一词）。如果我弄错了，我很抱歉！
不，@Fezvez，我认为您通常是对的，这就是我指定离散域的原因。对于具有无限域的变量，不可能有格式良好的 CNF，因为需要无限数量的变量。对于有限域，我们可以扩展一阶逻辑的 anys 和 exists 以在谓词逻辑中创建一个（长）语句序列。

标签： logic artificial-intelligence constraints constraint-programming conjunctive-normal-form

【解决方案1】：

您不妨考虑比利时鲁汶 Katholieke Univ 的 IDP3：http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 命题化一阶理论（通过归纳定义、聚合、有界算术键入一阶逻辑）并应用 minisat。

另一个选择是来自 Koen Claessen（瑞典查默斯大学）的 Paradox。 Paradox 是一阶逻辑的有限模型查找器，它也从转换为 SAT 开始，然后使用 MiniSAT 求解公式。 Paradox的源码可以从http://www.cse.chalmers.se/~koen/code/下载

【讨论】：

Alexander，这些看起来几乎正是我所需要的，但我早就离开了这个项目。因此，我想知道......您是否有自己使用它们的经验，您可以联系起来？（你是怎么找到悖论的？）
亲爱的理查德，我拿到了博士学位。来自鲁汶，所以我知道那里活跃着什么样的话题。但是，我没有使用任何这些工具的经验。
感谢您的帮助，@Alexander。有时间我会尝试测试这些，看看它们对我有什么作用，但与此同时，我会留下这个问题，以防它引起更多的思考。