问题标签 [first-order-logic]

我正在学习自然演绎和练习 Coq。

我们考虑一个公式：

现在我为可证明性添加了一堆推理规则：

但我坚持使用引言的暗示规则。我试过这个：

，这显然不起作用，因为归纳案例出现在否定位置。

蕴涵的引入规则是：

如何为 Coq 中的蕴含引入规则建模？

我不太清楚这个例子。该示例取自描述逻辑手册。

在示例的最后一行，“需要归纳，因此这种推理不是一阶的”。那条线完全让我措手不及。

你的解释很受重视。

早上好，我想了解如何使用一阶逻辑来描述某些东西。

例如，我想描述什么是电影（一个实体），什么是电影的属性（例如演员：克鲁尼）。我如何使用一阶逻辑来描述它？

******* 更新 ********

我需要按第一逻辑顺序解释的是：

ENTITY：可以用一组属性或属性描述的元素、抽象或对象。所以我认为我必须说实体有一组具有各自值的属性。实体描述一个元素、一个抽象或一个对象。

ATTRIBUTE：一个属性总是有一个值并且它总是与一个实体相关联。它描述了实体的特定特征/属性。

DOCUMENT：纯文本描述（纯文本，不包含任何 html 标签）。每个文档通过其属性仅描述一个实体。

对于任何给定的逻辑程序，它的证明理论使用 SLD（选择性线性定）分辨率来找到查询的可满足性。对于相同的逻辑程序，我们可以应用不动点定理来找到模型。

我的问题是，

我们应该考虑将逻辑程序的不动点作为证明理论或模型理论，还是两者都不是？

我不确定何时使用全称量词或存在量词。这是我的例子：任何通过历史考试并赢得彩票的人都很高兴。一阶逻辑：∀x Pass(x,history) ^ win(x,lottery) -> happy(x) 或 ∃x Pass(x, history) ^ win(x,lottery) -> happy(x) 我会想知道逻辑是否正确。

我对 Coq 处理存在量化的方式感到困惑。

我有一个谓词 P 和一个假设 H

而当前的目标是（无论如何）

如果我想在 H 中实例化 n，我会做

但是淘汰之后，现在的目标就变成了

看起来 Coq 将存在量词转换为通用量词。我知道(forall a, P a -> Q a) -> ((exists a, P a) -> Q a)出于我对一阶逻辑的有限知识。但相反的命题似乎是不正确的。如果 'forall' 和 'exists' 不等价，为什么 Coq 会进行这样的转换？

Coq 中的“elim”是否用更难证明的目标代替了目标？或者谁能​​说明为什么((exists a, P a) -> Q a) -> (forall a, Pa -> Q a)在一阶逻辑中成立？

我已经从使用 Int 切换到 SMT 中的位向量。但是，逻辑 QF_BV 不允许在您的脚本中使用任何量词，我需要定义 FOL 规则。我知道如何消除存在量词，但全称量词？怎么做？

想象一下这样的代码：

我正在阅读实用逻辑和自动推理手册。它有一些代码来定义文件中的有限部分函数 lib.ml。我无法理解部分函数中重新定义和组合的代码的含义。子功能的目的是什么newbranch？代码如下：

你能为我解释一下这段代码的含义吗？

我有这些事实（el代表大象）：

现在，我想证明（？）：Some gray lion like some pink像是： (exists x)(el(x) /\ gray(x) /\ (exists y) (el(y) / \ pink(y) /\ likes(x, y)). 所以，我们需要把它的否定和resolve(?) 化为基，才能得到void(?)。

否定是（将用于~显示否定）：

在我看来，我将分配x值y（Sam、Clyde 或 Oscar）并将后面的语句插入基础中，以“杀死”已经存在的事实。

我的尝试：

我设置x = Clyde, y = Oscar了，这给了我：

如果我把它放入基地，“杀死”他们的“对”，基地变成：

现在呢？我们的大象用完了！

理想情况下，我想拥有x' = Oscar, y' = Sam，这样我会得到：

它将进入基地并杀死一切，但~el(Oscar)仍然活着！我应该如何进行？

后续问题：

根据：

然后我把它放进基地~a/\~b/\~c/\~d。基地里的一切都会以同样的方式消失？我的意思是操作员不会V影响事情吗？

我正在做人工智能现代方法书中的一项练习。

这是问题：将英语转换为 FOL

而且，这是给它的答案。

我的疑问是。

我们通常使用带有通用量词的蕴涵，但在这里他们使用

(∃ y ∀ t Person(y) ∧ Fools(x, y, t))

对于这部分问题-can fool some of the people all of the time

这不是错的吗？

但是，在第二种情况下

他们使用了暗示。

我对存在量词和通用量词的顺序感到困惑。

有人可以消除我的疑问吗？

谢谢你。