问题标签 [first-order-logic]

我已经非常仔细地查看了文档和指南，并自己尝试了一些事情。然而，我的问题的解决方案却让我望而却步。

这是本教程关于记录的内容，但我不清楚如何让它适合我的需要：

我正在寻找用于声明5 个字段、2 个整数和 3 个布尔值的记录的 SMT-LIB2 语法。

然后我想要一个数组/一组这些记录。

我还在寻找我将用来在某些记录集上创建 $\forall$ 语句的语法。

我尽力利用所提供的资源，但一无所获。

谢谢。

我正在尝试使用自动定理证明器 SPASS 在一阶逻辑中对一些硬件进行建模。

所以我需要可以采用真/假值（预定义的值）的信号，以便能够在逻辑语句中使用它们。

SPASS 支持用户可以自己定义的某种类型（称为排序）。

我想知道是否有一些预定义的真/假类型？

我想即使没有类型，我也可以解决这个问题。通过使用 True(SIGNAL) 和 False(SIGNAL) 形式的谓词，并在 SIGNAL = T 时使 True(SIGNAL) 返回 true，在 SIGNAL = F (T 和F 是常量），但我认为使用预定义的真/假会更好。

我已经设法使用 Z3 创建了一个记录数组，但现在正在努力查看在数组上执行 $\forall$ 操作所需的语法......这是我到目前为止的 SMT-LIB2 代码片段示例.

我想倒数第三行应该对数组有一些参考，但我已经尝试了一切，教程并没有帮助我解决这个问题。

如何对这里的数组执行 $\forall$ 操作？

我一直在阅读有关将自然语言句子转换为一阶逻辑的文章，我很好奇如何在一阶逻辑中表达逻辑推理。

我想知道如何将“由于事件 B 发生事件 A”之类的句子转换为一阶逻辑。

我能想到的这样一句话的一个例子是：

上面的句子是如何用一阶逻辑表示的？

我想到的解决方案是：

但是我不确定这是否正确，因为我在网上找不到类似句子的例子。如果这是错误的，为什么它是错误的，我该如何纠正它？

超级基础的问题。我试图表达两个二元谓词（父母和孩子）之间的对称关系。但是，通过以下陈述，我的解决方案证明者允许我证明任何事情。转换后的 CNF 形式对我来说很有意义，解析证明也是如此，但这应该是一个明显的错误案例。我错过了什么？

我正在使用 nltk python 库和 ResolutionProver 证明者。这是nltk代码：

输出：

我的直觉说不可能翻译句子

所有红色汽车都比所有蓝色汽车好

进入描述逻辑（在 FOL 中，这将是

∀x∀y（红色（x）∧蓝色（y）→更好（x，y））

在汽车领域进行解释）。实际上，包含域的所有元素对的完整二元关系的唯一构造是通用角色U。我看不到如何要求左侧集合红色的所有元素对和右侧集合蓝色的元素，即如何将U限制为一组特定的前任和后继。

但不知道如何去做并不能证明这是不可能的。因此我的问题是：当您使用特定类型的描述逻辑（例如此处描述的SROIQ）时，您如何证明不可能在其中表示给定的自然语言句子或 FOL 公式？

我目前正在学习 FOL，并且有一些我正在尝试将其表述为 FOL 语句的英语语句。

我有英语陈述以及我在每个方面的 FOL 尝试。我只是想知道是否有人可以让我知道我是否以及在哪里出错了，谢谢。

英语陈述

1. 一个高个子可以达到一个高钩。

2. 一个小个子可以达到一个低钩。

3. 高钩是免费的。

4. 如果有一个免费的衣帽钩，一个男人会挂他的外套，并且这个男人可以够到那个衣帽钩。

5. 保罗是个高个子。

6. 约翰是个矮个子。

7. 谁能把他们的外套挂在什么挂钩上？

一阶逻辑语句尝试

1. ∀x man(X, tall) ->reach_hook(X, high_hook)。

2. ∀x man(X, small) ->reach_hook(X, low_hook)。

3. 免费（high_hook）。

4. ∀x,y free(X) ^reach_hook(Y,X) -> hang_coat(Y, X)。

5. 男人（保罗，高）。

6. 男人（约翰，短）。

7. ?- hang_coat(X,Y)。

我正在查看一阶逻辑定理证明器，例如 Vampire 和 E-Prover，TPTP 语法似乎是要走的路。我更熟悉诸如答案集编程和 Prolog 之类的逻辑编程语法，虽然我尝试参考TPTP 语法的详细描述，但我似乎仍然没有掌握如何正确区分解释和非解释函子（我可能使用错误的术语）。

本质上，我试图通过证明没有模型作为反例来证明一个定理。我的第一个困难是我没想到下面的逻辑程序是可以满足的。

这确实是可满足的，因为没有什么能阻止bar等于foo。所以第一个解决方案是坚持这两个项是不同的，我们得到以下不可满足的程序。

技术报告澄清了不同的双引号字符串确实是不同的对象，所以另一种解决方案是在这里和那里加上引号，从而得到以下无法满足的程序。

我很高兴没有手动指定不等式，因为这显然不会扩展到更现实的场景。更接近我的实际情况，我实际上必须处理组合术语，不幸的是，以下程序可以满足。

我猜f("foo")这不是一个术语，而是f应用于对象的函数"foo"。所以它可能与 function 重合g。尽管一个从不重合的手动规范可以解决问题f，g但以下程序不能令人满意，我觉得我做错了。而且它可能无法扩展到我的真实环境，当它们在语法上不同时，所有术语都被解释为不同的。

我尝试过使用单引号，但没有找到正确的方法。

如何使句法不同（组合）的术语和测试句法相等？

辅助问题：以下程序是可满足的，因为自动定理证明器将其理解f为函数而不是未解释的函子。

为了使它无法满足，我需要手动指定 f 是单射的。在不指定我的程序中出现的所有仿函数的注入性的情况下，获得这种行为的自然方法是什么？

Prolog 规则如下：

一阶逻辑将是：

理论上，如果我们的 Prolog 规则中有一个匿名变量，例如：

假设它是一个姓氏，我们如何以一阶逻辑呈现它？

一阶逻辑的有效命题 (EPR) 片段通常被定义为形式为 的一组前置量化公式∃X.∀Y.Φ(X,Y)，其中X和Y是（可能为空的）变量序列。量化的顺序，即∃*∀*EPR 的可判定性是否重要？如果量化顺序被切换，我们会失去可判定性吗？

特别是，我对在可判定逻辑中捕获 set-monadic 绑定操作的语义感兴趣。给定一组S1类型的元素T1（即，S1具有类型T1 Set）和一个f类型的函数T1 -> T2 Set，set-monad 的绑定操作通过对 的每个元素应用并合并结果集来构造一个新S2的类型集。可以在以下 SMT-LIB 代码/公式中捕获此行为：T2 SetfS1

观察到第二个断言语句有量化的形式∀*∃*，它不符合标准的 EPR 定义。然而，在 Z3 上使用此类公式时，我从未遇到过超时问题，我想知道我上面的公式是否确实在某个可判定的片段中（同时承认实践中的可解性并不意味着理论上的可判定性）。欢迎任何意见。