标签: theorem-proving

我是二年级学生，我的离散数学 2 作业是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序（假设证明始终存在）。到目前为止，我已经用谷歌搜索过，但 4 周后，那里的材料真的很难理解。谁能给我推荐一些适合初学者的书籍/网站/开源代码或一些有用的提示？先感谢您。

有时<statement> solve_direct（我通常通过调用<statement> try）列出一些库定理并说“当前的目标可以直接解决：……”。

设<theorem>一个搜索结果solve_direct，然后在大多数情况下我可以证明<statement> by (rule theorem)。

然而，有时这样的证明不被接受，导致错误信息“应用初始证明方法失败”。

是否有一种通用的、不同的技术来重用由 找到的定理solve_direct？

还是要看个人情况？我可以尝试找出一个最小的例子并将其附加到这个问题上。

在 Isabelle，我经常发现我可以使用不同的求解器成功地证明一个目标。

通常，我更愿意使用可以证明目标的最弱求解器。根据我目前与 Isabelle 的经验，我目前的理解是，按照强度增加和速度降低的顺序，常见的逻辑求解器排名如下（即何时rule和simp两者都起作用，rule应该使用等）：

rule < simp < auto < fastforce < force

这样对吗？这里blast适合放哪里？

我检查编程和伊莎贝尔/ HOL（PDF）证明和与伊莎贝尔/ HOL具体语义，但无法找到答案。

问题

我想知道在 Isabelle 中是否有一种自然的编码方式是这样的语法：

 type_synonym Var = string
 datatype Value = VInt int | ...
 datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ...

动机是根据非确定性选择定义一些规范命令，例如：

 Magic == NonDeterministicChoice {}
 Rely c r z = Defined using set compreehension and NonDeterministicChoice

Isabelle 抱怨“Cmd set”中类型“Cmd”的递归出现，即：

不支持通过类型表达式“Cmd set”中的类型构造函数“Set.set”递归出现类型“Cmd”。使用“bnf”命令将“Set.set”注册为有界自然函子以允许嵌套（共）递归通过它

在我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为“set”类型注册有界自然函子，因此我决定尝试一种推测性解决方案。

投机解决方案

相反，如果我使用归纳定义的数据类型，例如列表，伊莎贝尔不会抱怨，例如

datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...

列表在这里不是正确的抽象，但我试一试看看它是否有效。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题就变成了假设存在两个列表：一个包含Cmd 的所有元素，另一个包含Value 的所有元素。

我声明了两个未解释的常量：

consts Values :: "Value list"
consts Programs :: "Cmd …

我正在尝试编译一个 Agda 文件，但是我无法让它找到标准库。我在这里看过文档。

我使用 Stack 来安装它：

> which agda
/home/joey/.local/bin/agda

我已经为我的 Agda 目录设置了环境变量：

> echo $AGDA_DIR
/home/joey/.agda

其中填充了正确的文件：

/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/libraries
/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/defaults
standard-library

> cat /home/joey/agda/agda-stdlib/standard-library.agda-lib
name: standard-library
include: src

但是，当我去编译 Agda 文件时，出现以下错误：

Failed to find source of module Function in any of the following
locations:
  /home/joey/agda/AutoInAgda/src/Function.agda
  /home/joey/agda/AutoInAgda/src/Function.lagda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.agda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.lagda
when scope checking the declaration
  open import Function

我如何告诉 Agda 去哪里寻找标准库？这是因为堆栈的问题吗？

我在 Ubuntu 17.10 上，如果这有区别的话。

我想证明涉及矩阵和向量的表达式的属性（可能很大，但大小是固定的）。

例如我想证明一个表达式的结果是对角矩阵或三角矩阵，或者是正定的，...

为此，我想从线性代数中编码众所周知的属性和身份，例如：

||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
det(A+B) = det(A) + det(B)
Tr(zA) = z * Tr(A)
(I + AB) ^ (-1) = I - A(I + BA) ^ (-1) * B
...

我试图在 Z3 中实现这一点。但即使对于简单的属性，它也会返回未知或超时。我尝试过数组理论和量词。

我想知道这个问题是否可以用 SMT 求解器解决，还是不适合这类问题？你能举一个小例子来暗示吗？

我正在阅读伊德里斯教程。而且我无法理解下面的代码。

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = () 
    disjointTy (S k) = Void

到目前为止，我发现......是 Void空类型，用于证明某些事情是不可能的。

替换：(x = y) -> P x -> P y 替换使用等式证明来转换谓词。

我的问题是：

1. 哪一个是平等证明？(Z = S n)？

2. 哪一个是谓词？功能disjointTy？

3. 目的是什么disjointTy？disjointTy Z = () 是否意味着 Z 位于一个类型“land”() 中且 (S k) 位于另一块土地中Void？

4. Void 输出以什么方式表示矛盾？

诗。我所知道的证明是“凡事不匹配则为假”。或者“找到一件矛盾的事情”......

我工作在以下定理的证明Sn_le_Sm__n_le_m中IndProp.v的软件基础（第1卷：逻辑基础）。

Theorem Sn_le_Sm__n_le_m : ?n m,
  S n ? S m ? n ? m.
Proof.
  intros n m HS.
  induction HS as [ | m' Hm' IHm'].
  - (* le_n *) (* Failed Here *)
  - (* le_S *) apply IHSm'.
Admitted.

其中，的定义le (i.e., ?)是：

Inductive le : nat ? nat ? Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : …

我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共导和共模式。我以为我理解文章代码，所以我决定研究以下命题。

cons-uncons-id : ? {A} (xs : Stream A) ? cons (uncons xs) ? xs

我以为这个命题和文章问题非常相似，也可以证明，但我不能很好地证明。 这是我写的代码。

我认为它可以改进，cons-uncons-id (tl xs)因为它的类型与 merge-split-id 非常相似，但 Agda 不接受它。

这是我自己想到的一个问题，所以我认为这是真的，但当然存在误解的可能性。然而，非利弊和利弊会恢复原状是很自然的。

如果你应该能够证明它而不会被误解，请告诉我你如何证明它。

你能解释一下为什么不能像merge-split-id一样证明吗？

问候，谢谢！

有时我发现很难使用 Isabelle，因为我无法像在正常编程中那样使用“打印命令”。

例如，我想看看什么?thesis. 具体语义书说：

未知 ?thesis 隐含地与引理或 show 陈述的任何目标相匹配。下面是一个典型的例子：

我的愚蠢示例 FOL 证明是：

lemma
  assumes "(? x. ? y. x ? y)"
  shows "(?x. ? y. y ? x)"
proof (rule allI)
  show ?thesis

但我收到错误：

proof (state)
goal (1 subgoal):
 1. ?x. ?y. y ? x 
Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  ?x. ?y. y ? x

但我知道为什么。

我期望

?thesis === ?x. ?y. …