问题标签 [theorem-proving]

我正在阅读 B.Russell 的《数学哲学导论》一书，并试图将其中描述的所有定理形式化。

一对多关系由以下文本描述（书上的上下文）。

一对多关系可以定义为这样的关系，如果 x 与 y 有关系，则没有其他项 x' 也与 y 有关系。

或者，它们也可以定义如下：给定两个项 x 和 x'，与 x 具有给定关系的项和与 x' 有关系的项没有共同的成员。

或者，再一次，它们可以被定义为这样的关系，使得它们中的一个及其逆的相对乘积意味着同一性，其中两个关系 R 和 S 的“相对乘积”是当存在一个中间项 y，使得 x 具有 R 与 y 的关系，y 具有 S 与 z 的关系。

它提出了三种定义方式。我已经成功地描述了前两个并证明了它们的等价性。当我被困在第三个时，我试图摆脱“相对产品”的概念，直接进入它的内涵，但也失败了。

以下是我的定义，我犯了什么错误吗？

以下是我如何解释第三个的定义，我也未能证明它们的等价性。

其中证明id_eqv是Lemma id_eqv : forall {X} (x:X) (y:X), x = y <-> id x y，很容易预先证明。

有人可以帮我弄清楚或给我提示我哪里出错了吗？提前致谢。

快速复审：

• 推理规则=结论+规则+前提
• 证明树 = 结论 + 规则 + 子树
• 后向证明搜索：给定一个输入目标，尝试通过自下而上的方式应用推理规则构建证明树（例如目标是最终结论，应用规则后会生成新的子目标列表现场）

问题：
给定一个输入目标（例如A AND B,C），假设我们首先在 上应用规则 AND A AND B，然后得到两个新的子目标，第一个是A,C，第二个是B,C。
问题是A和B是无用的，这意味着我们可以只使用C. 但是，我们有两个子目标，那么我们要证明C两次，所以效率很低。

问题：
例如，我们有A AND B,C AND D,E AND F,G,H AND I. 在这种情况下，我们只需要 D 和 G 来构建完整的证明树。那么如何选择正确的规则来应用呢？

这是 Ocaml 中的示例代码：

关系代数REL051+1.p中的问题读取

使用 TPTP 语法和 fof 对应的代码是

正如您在TPTP中看到的，所有 ATP 都无法证明此类问题。

使用以下 SMT-LIB 用 Z3 驳斥了该定理

相应的输出是

请在此处在线运行此示例

我的问题是：这个对 Z3 的反驳是正确的吗？

我正在尝试对依赖函数进行证明，但遇到了障碍。

所以假设我们有一个定理 f-equal

我试图证明一个更一般的概念，即在依赖函数上保持平等，但遇到了障碍。即，类型

使编译器不高兴，因为它无法确定 fx 和 fy 属于同一类型。这似乎应该是一个可以解决的问题。是吗？

笔记; 使用的等价关系定义如下：

我（错误地）学习了一门关于验证并发程序的课程，到目前为止，我们已经介绍了这种称为“Owicki-Gries 方法”的方法。显然，可以通过将断言与每个语句相关联来证明程序的各种结果，并表明这些断言是归纳的并且不会相互干扰。我们的一项任务涉及 Lamports 的快速互斥算法，详见本文：

在论文中，给出了互斥的 Owicki-Gries 风格证明。它看起来完全违反直觉。我很难理解的是如何首先提出这些断言？你什么时候知道这些断言既不是太强（太强以至于它破坏了干涉自由）也不是太弱（例如一些微不足道的东西，比如每个陈述的重言式）？

干杯

输入是具有（任何）已检查语法的符号字符串，输出为 TRUE 或 FALSE。

我的想法是用 AND、XOR 和 TRUE 编写的逻辑表达式的 post-fix 表示，但我最终意识到在 post-fix 中这些模式将更难识别。

例子：

p 意味着 q可以写成TRUE XOR p (XOR (p AND q))缩写 1+p+pq

p EQUIVALENT WITH q可以简写为 1+p+q

NOT p缩写 1+p

p OR q缩写为 p+q+pq

这个布尔环中的规则与普通代数中的规则相同，有两个规则

• p+p=0
• pp=p

并且这些规则连同交换一起负责所有减少，如果字符串对应于重言式，这将导致“1”。重言式 Modus ponens，

((p 暗示 q) 和 p) 暗示 q ,

应先如上代入，然后分布乘法展开，最后反复化简。直接替换 IMPLIES 给出：

当一个重言式表达式被写成布尔环中的一个元素时，它会机械地归约为 1。其他表达式归约为代数上更简单的表达式。

这是一个好策略吗？计算机科学中使用了哪些策略？

我正在使用 Coq 完成一些介绍级别的组合逻辑练习。我已经为它编写了一个粗略的库，但它不是很有效。是否有用于 Coq 或其他证明助手的组合逻辑库？组合子、术语及其关系的定义以及一些重要定理的证明将非常有帮助。

有一个关于 Agda 和组合逻辑的讨论看起来很有趣，但我不知道它是否与我的问题相关。

我正在尝试使用 Z3 来求解涉及未知投影函数的方程，以找到满足方程的函数的有效解释。例如，对于等式：snd . f = g . fst一个有效的解释是f = \(x,y) -> (y,x)和g = id。我知道 Z3 不是更高阶的，所以我一直在尝试以一阶形式对问题进行编码。因此，例如对于f = g.fst我使用：

返回的作品类型：

但是对于snd . f = g . fst（我已经将树简化为对尝试和帮助）：

我明白了unknown。

我还尝试在不使用 ADT 的情况下仅使用布尔值或整数作为参数来编码类似的问题，但是模型只是将常量值分配给函数。我还尝试为函数常量、恒等函数以及成对和顺序组合定义一个简单的 ADT，然后定义一个可以简化表达式的“等于”函数，例如f.id = f，但这要么涉及递归函数，例如：

这显然是无效的。或者，如果我使用未解释的函数，它会使“eq”成为常量函数，即

与涉及 Int -> Int 类型函数的方程类似，这将返回 f 和 g 的常数函数：

并添加这些时间：

有什么想法可以让这种事情发挥作用吗？

非常感谢！

我正在 youtube 上观看有关分辨率的视频，并看到了这个视频，它对我有很大帮助：

http://www.youtube.com/watch?v=hhTxW5c3BXo

接近尾声时，他做了一个例子，其中每个子句中相对侧的 X 都被抵消，其余的被连接在一起，这没关系，但我想知道它是否适用于多个变量抵消，例如：

(AB -> CDXY) (PQXY -> RS)

取消 XY 将给出 ABPQ -> RSCD

我有这种直觉，这种“双重分辨率”的情况不适用，而且我无法找到任何有关取消 2 个或更多变量的信息。

有什么我想念的吗？

使用 Z3 可以证明

形成一个单参数组。

使用以下 Z3 代码执行证明：

相应的输出是

请在此处在线运行代码。

其他例子：证明

形成一个单参数组。

使用以下 Z3 代码执行证明：

相应的输出是

请在此处在线运行此代码

其他例子：证明

形成一个单参数组。

证明在这里在线给出，四维扩展在这里在线给出

最后几个例子：证明

形成一个单参数组。

证明在这里在线给出。

证明

形成一个单参数组。

证明在这里在线给出。

更一般地，证明

形成一个单参数组。

证明在这里在线给出。

一个三维扩展：证明

形成一个单参数组。

证明在这里在线给出。

双曲函数的一个例子：证明

形成一个单参数组。

证明是在网上给出的 here

我的问题是：

1. 可以使用数组来证明更高维度吗？

2. 我声称 Z3 是唯一能够执行这些证明的系统。你同意吗？