问题标签 [first-order-logic]

我正在阅读有关 Coq 的教程。它构造一个bool类型如下：

然后它显示了这些东西中的每一个都在使用“检查”。

我明白了bool_ind。它说，如果某事物成立true并且它成立false，那么它成立于所有b（bool因为这是唯一的两个）。

但我不明白这些表达是什么bool_rec意思bool_rect。似乎P true（这是 a Setforbool_rec和 a Typefor bool_rect）被视为命题值。我在这里想念什么？

我正在研究一个本体来表示星际争霸中的信息，但我无法确定以下通用类公理是否可以在 DL 中表示。如果没有，我想知道表达它所需的最小逻辑集（FOL、二阶等）。

有了这个公理，我想表示一个玩家控制一个区域，如果（1）该区域存在一个单位，并且（2）该区域中的每个单位都归玩家所有。

我有3个角色：

A. controlsRegion(p,r) 其中 p 是玩家，r 是区域

B. isOwnedBy(u,p) 其中 u 是一个单位，p 是一个玩家

C. isInRegion(u,r) 其中 u 是一个单位，r 是一个区域

没有足够的代表来发布图片，请参见此处的公式：http: //postimg.org/image/wve0h9m1z/

u、p 和 r 是变量（这就是为什么我不相信这可以在 DL 中表示）

另外，我不确定我使用的语法是否正确，请告知如何正确表示它。

谢谢，任何反馈表示赞赏！

正如标题所说，我正在尝试解析例如

在 Lua 表中

这是我建立的语法：

我有以下问题：

• 它无法解析嵌套术语。对于上面的示例，它仅返回{term, {} }（虽然可以使用term(A, b, c)）。
• 要从我使用的字符串中去除引号{~ ~}，但正因为如此，我必须从下面的行中移动所有argument捕获term。有没有办法避免这种情况？
• 我想有一个与每个元素关联的键来指定它的类型，例如，而不是A像{value = "A", type = "variable"}. 我找到了一种方法来做到这一点，{:name: :}但是，表中元素的顺序丢失了（因为它不会创建一个新表，而只是添加一个键，在这种情况下variable="A"，这个元素的顺序是不固定的）。如何标记维持订单的物品？

LOAD关键字将映射到哪种关系代数运算符？如果它不是逻辑运算符而只是物理运算符，那么在数据库查询处理器的逻辑到物理运算符转换过程中如何处理它？或者，如果它没有映射到关系代数原语，那么它是否是特定于实现的关系代数运算符扩展？

我很难用一阶逻辑表达以下想法。

我想说每个代理都有一个初始位置，我会这样表达（使用文字）：

对于 Agents 类型的所有代理，存在 xCoordinate 类型的 x 和 yCoordinate 类型的 y，使得 I_Position(agent,x,y) AND Tile(x,y)

或在 idp 中：

瓦片是一个有效瓦片的表达式，一个有效的位置。

这个表达式的问题是，我了解到一个For All表达式总是带有暗示 ( =>)，而There Exists表达式总是带有 And ( &)。

显然，我没有暗示。这句话和我想的一样吗？

我正在尝试实现一个采用 FOL 语句并以子句形式返回等效语句的函数。任何关于链接的想法，样本，因为我找不到任何到目前为止。

我认为这总是正确的

相当于

如果是这样，那条法律叫什么？我什至不确定我会如何谷歌。

你能告诉我命题逻辑和一阶逻辑有什么区别吗？这是我在人工智能中的一个考试题，你能帮我做吗

我开始研究 Mercury 语言，这似乎很有趣。我是逻辑编程的新手，但对 Scala 和 Haskell 的函数式编程非常有经验。我一直在思考的一件事是，当您已经拥有至少应该与类型一样具有表达力的谓词时，为什么在逻辑编程中还需要类型。

例如，在以下代码片段中使用类型有什么好处（取自 Mercury 教程）：

与仅使用谓词编写它相比：

请随意指出涵盖该主题的介绍性材料。

编辑：我可能对问题的表述有点不清楚。实际上，我是在研究了 Idris 等依赖类型语言之后才开始研究 Mercury 的，就像在依赖类型中可以在类型中使用值一样，也可以在编译时使用谓词来验证逻辑程序的正确性。如果程序需要很长时间来评估，我可以看到出于编译时性能原因使用类型的好处（但前提是类型不如“实现”复杂，在谈论依赖类型时不一定是这种情况）。我的问题是除了编译时性能之外，使用类型是否还有其他好处。

给定句子： 1.Tom 有一台不错的笔记本电脑 2. 只有当 Mary 去餐厅时，Tom 才会去餐厅

我将如何将其转换为命题逻辑和谓词逻辑。我试着试一试，但我不确定它是否正确。

这个对吗？