问题标签 [first-order-logic]

在研究描述逻辑 (DL) 时，很常见的是它是一阶逻辑 (FOL) 的一个片段，但是很难明确地阅读 DL 中排除的内容，这是 FOL 的一部分，这使得 DL （及其所有方言 ALC、SHOIN 等...）可判定。或者换句话说，您能否在 FOL 中提供一些无法通过 DL 表达的示例（这也是 FOL 中半/不可判定性的原因）？

是否存在能够将英语句子翻译成一阶逻辑的工具或库？

例如：“所有爱全人类的东西都是狗。” 变成：

我认为它被称为语义解释器，但除了研究论文之外，我似乎没有找到任何东西。

我刚刚开始学习 Java 和自然语言处理，如果我的问题之前已经回答过（或者如果它很愚蠢），我提前道歉。

谢谢你的帮助。

我一直在阅读一些关于将一阶逻辑 (FOL) 句子转换为连接范式 (CNF)，然后执行解析的笔记。

转换为 CNF 的步骤之一是Standardize variables.

如果我不标准化变量，我一直在寻找为什么解析算法的完整条件违反并且健全性不违反。

任何人都可以添加细节，为什么只是违反完整性，而完整性仍然存在？

使用逻辑编程符号，给定以下子句：

可以用 C' 的第一个正文文字来解析 C 的头部，以给出替换{P/Q',X/X'}和子句：

我怎样才能用 Prolog 展示这个？换句话说，我怎样才能证明你可以D从C?

我正在尝试使用 Haskell 实现 FOL。一阶逻辑可以是命题的形式，通过 And 和 Or 等连接词连接在一起。还有一些量词在表达式中具有有限的范围。

到目前为止我所做的是：

导入数据列表

但我收到此错误：

我想在合金中写一个集合和一个关系之间的双射。

例如，在下面的代码中，我想将 ref 定义为 QArow 和 event 之间的双射。因此，我写了事实bij。但是 Alloy 抱怨说，因为我认为我量化了使bij事实中的两个表达式成为高阶逻辑表达式的关系：

如何将这些表达式转换为一阶逻辑表达式？

另外，一般来说，当我们可以将 HOL 表达式转换为 FOL 表达式以及何时不能这样做时，是否有任何指导方针？

谢谢

lexpr 到底是什么意思，下面的 r'/F xx 是什么意思？还有什么是应用程序表达式？

我需要在 Prover9 中为以下谜题建模

一个港口有5艘船：

1. 希腊船六点出发，载着咖啡。
2. 中间的船有一个黑色的烟囱。
3. 英国船九点出发。
4. 带有蓝色烟囱的法国船在运送咖啡的船的左侧。
5. 载可可的船的右边是一艘前往马赛的船。
6. 这艘巴西船正驶向马尼拉。
7. 载米的船旁边是一艘带有绿色烟囱的船。
8. 一艘去热那亚的船五点出发。
9. 西班牙船七点出发，在前往马赛的船的右侧。
10. 带有红色烟囱的船前往汉堡。
11. 七点出发的船旁边是一艘带白色烟囱的船。
12. 边境的船载着玉米。
13. 黑烟囱的船八点出发。
14. 运送玉米的船停泊在运送大米的船旁边。
15. 六点开往汉堡的船。

哪艘船去塞得港？哪艘船运茶？

据我所见，prover9 接受一阶逻辑子句。但我真的不擅长将自然语言转换为 fol。有人可以告诉我如何以一阶逻辑对此进行建模，也许可以告诉我如何转换第一条语句？

在尝试用 groovy 中的闭包重新发明 if/else 语法时，我无法让它工作。我认为在括号外放置多个闭包是不允许的，但它可能是别的东西。

如果不允许，您将如何重现 if/else 语法？这是一个思想实验，所以不要告诉我这个实现的效率低下。

我的代码：

错误信息：

java.lang.NullPointerException：无法在空对象上调用方法 ifx()

谁能帮我证明：

公式 F 的一个实例的全封闭是 F 的全封闭的逻辑结果。

谢谢。