问题标签 [first-order-logic]

我尝试用否定的请求询问知识库。所以在解决之前，补码（这里是positif）被添加到算法使用的子句集中。

有了这些事实：

和论文公理：

子句变成 CNF

我可以要求

配偶（莎拉，安德鲁）或配偶（苏菲，爱德华）

这个请求 ¬Spouse(Sarah,Edward) : Sarah 不是 Edward 的配偶，不工作。

当然，我可以问配偶（莎拉，爱德华）是否是莎拉与爱德华的配偶，没有答案，认为这是错误的。

这种请求有什么问题，因为我不知道我的实现是否存在错误，或者是否不可能这样做（假设是......）。

谢谢你的帮助 ！

我希望能够在 ASP/cligo 中制定以下 FOL 语句：

两者的域X由Y给出dom/1。的域A由 给出domA/1。的域V是1..n。

对我来说，问题是混合量化。现在，当然，我可以扩展∀ V并得到如下内容：

但是，当我n直到运行时才知道（我将它作为参数传递给 cligo）时，这并不能很好地工作。

有没有办法用 cligo 方便又干净地做到这一点？还是应该改用 Python/Lua 脚本功能？如果是这样，怎么做？

我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们对使用量词解决 SMT 问题的能力都有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述了可能实际实施或未实施的可能变化。

我知道一阶逻辑有可判定的片段，例如：

• 有界量词
• 一阶一阶逻辑

我想知道的是，哪些（如果有的话）FOL 类是保证完成的各种 SMT 求解器？我如何知道我正在查看的问题是否存在于它们完成的片段中？

一阶一阶逻辑，其中所有谓词都只有一个参数，是一阶逻辑的已知可判定片段。测试一个公式在这个逻辑中是否可满足是可判定的，并且存在基于分辨率的方法来判定这一点。

我处于需要测试一些一阶一阶逻辑语句的可满足性的情况。我意识到我将达到复杂性的理论极限，但我希望我能在常见情况下获得合理的性能。

目前，存在大量的定理证明器，它们为解决一阶逻辑问题提供了快速的方法。这些包括Vampire、SPASS、E，以及Z3和CVC4的量词扩展。但是，由于不确定性，它们不能保证停止。

我的问题

在现有的定理证明者中，当给定一元公式作为输入时，是否有任何人可以保证停止？或者有没有办法使用它们（在某种程度上）有效地测试一元公式的可满足性？

我到处寻找我能找到的关于这个主题的任何信息，但我找不到任何东西。甚至我的教科书也完全跳过了它。

关于统一 Skolem 功能甚至一般功能的规则是什么？

任何人都可以有所了解吗？

我想知道我们如何为大学的员工使用描述逻辑语法（A-box，T-box）制作本体？我们可以在它们之间建立哪些类、对象、关系、父母、兄弟姐妹、约束和相互关系？

我制作了下面的类图，但不确定是否可以添加其他任何东西。

无火无烟，无烟无火。

用 Prolog 程序识别上述语句的结论和条件。在答案中，结论必须是，如果有火，就有烟，如果有烟，就一定有火。

我该怎么做呢？

请解释答案。

我有以下 FOL 公式：∀e(S(e)) → ∃d(P(d))

还有词汇：
variables: e:'exam', d:'day' functions: S:'successful', P:'party'

我最初将该公式翻译成：
For every successful exam, there will be a day of party

虽然显然正确的翻译是这样的：
You party at least one day after all exams were successful.

为什么正确的说我们只有在所有考试都成功后才聚会？

是否∀e(S(e))意味着：“对于所有考试，他们都会成功”？意思是： “∃d(P(d))至少有一天我们聚会”？

暗示不是转化为“if a then b”吗？

我想我可以以某种方式看到正确翻译的逻辑，但其中的含义让我不确定……

将下列语句翻译成 FOL 句子

1)亚历克斯喜欢约翰

Likes(alex, john) - 我知道这是正确的

2)每个人要么是男人要么是女人

AxAy（男人（x）v女人（y））

编辑：这更好吗？？： Az(Person(z) -> man(x) v woman(y)) 或编辑：这更好吗？？： Ax(Person(x) -> man(x) v woman( X））

3）没有人既是男人又是女人

例如（（男人（x）^ ¬女人（x））v（¬男人（x）^女人（x）））

4）Alex喜欢一个喜欢女人的男人

AxEy（喜欢（男人（x），女人（y））->喜欢（亚历克斯，男人（x）））

谢谢

这是背景信息的截图

编辑：对于第 3 号，我在网上找到了这个“p 和 q 的排他性析取断言 p 为真或 q 为真，但不是两者兼而有之。那么，表达排他性析取的自然但冗长的方式是(p | q) & ~(p & q)。”

如果这适用，那么我假设正确答案是 Ax( (man(x) v woman(x)) ^ ¬(man(x) & woman(x)) )

但是现在我对2和3有何不同感到困惑......

我在下面有一个我编写的 prolog 程序的简单示例，其中包含一个可满足的查询，该查询始终返回 false 进行搜索。

当我问两个常量是否是兄弟时，这很好，但是如果我尝试找到一个常量 prolog 的兄弟，则返回 false。

我究竟做错了什么？