标签: 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）遇到的每一个可以解决的目标arith都可以通过解决，presburger反之亦然，例如

lemma "odd (n::nat) ? Suc (2 * (n div 2)) = n"
by presburger (* or arith *)

两个求解器有什么区别？一个目标可以解决而另一个却无法解决的目标示例。

编辑：我设法想出通过证明引理arith是presburger无法处理。似乎这与实数有关：

lemma "max i (i + 1) > (i::nat)" by arith       -- ?
lemma "max i (i + 1) > (i::nat)" by presburger  -- ?

lemma "max i (i + 1) > (i::real)" by arith      -- ?
lemma "max i (i + 1) > (i::real)" by presburger -- ?

我正在尝试编译一个 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 上，如果这有区别的话。

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

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 输出以什么方式表示矛盾？

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

自动定理证明的重要部分是通过弄清一个子句何时包含另一个子句来减少冗余。

直观地讲，子句（CNF中的一阶逻辑公式）C至少包含另一个子句D时，它会包含在内。具体定义是必须将变量替换为将C变成D的子多集的项。例如叠加。）

有一些索引技术可以极大地减少必须进行的包含尝试的次数，但是即使这样，包含也可以消耗大量的CPU时间，因此对其进行优化很重要。显然，在一般情况下它是NP难解的，但要使大多数特定情况下快速运行仍然是可能而且必要的。

以下伪代码是正确的，但效率不高。（在实践中，负和正文字必须分别处理，然后出现一些问题，例如尝试以双向方式定位方程，但是在这里，我仅考虑用于匹配两袋文字的核心算法。）

def match_clauses(c, d, map):
    if c == {}:
        return true
    for ci in c:
        for di in d:
            if match_terms(ci, di, map):
                if match_clauses(c - ci, d - di, map):
                    return true
    return false

为什么效率低下？考虑两个子句p(x) | q(y) | r(42)和p(x) | q(y) | r(54)。上面的算法将首先成功匹配p(x)，然后成功匹配q(y)，然后通知r(42)不匹配r(54)。好的，但是随后它将尝试另一种方法：首先成功匹配q(y)，然后成功匹配p(x)，然后再次注意r(42)不匹配r(54)。如果有N个文字确实匹配，那么浪费的工作将是N个阶乘，在某些实际情况下会严重降低效率。

如果有足够的时间，我无疑会想出一种更好的算法，但是其他人必须在我之前完成此操作，因此似乎值得一问：什么是最知名的算法？

我想验证假设当然也是的Ring实例。在 Abelian Group 之前这很容易，但在实例中发生了一些奇怪的事情：Data.Complex.Complex ttRingRing

VerifiedRing t => VerifiedRing (Complex t) where
    ringOpIsAssociative (l :+ li) (c :+ ci) (r :+ ri) =
        ?VerifiedRing_rhs_1

现在 Idris 自己进行了一些扩展，并且该洞得到以下类型：

(l <.> (c <.> r <+> inverse (ci <.> ri)) <+> inverse (li <.> (c <.> ri <+> ci <.> r))) :+ (l <.> (c <.> ri <+> ci <.> r) <+> li <.> (c <.> r <+> inverse (ci <.> ri))) =
((l <.> c <+> …

我正在努力使Coq中的Free Selective Applicative Functors正式化，但是我在通过归纳法对具有非均匀类型参数的归纳数据类型进行挣扎。

让我简要介绍一下我正在处理的数据类型。在Haskell中，我们将自由选择函子编码为GADT：

data Select f a where
    Pure   :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

关键是b第二个数据构造函数中的存在类型变量。

我们可以将此定义转换为Coq：

Inductive Select (F : Type -> Type) (A : Set) : Set :=
    Pure   : A -> Select F A
  | MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A. …

在以下程序中填补空缺是否一定需要非建设性的手段？如果可以，是否x :~: y可以决定？

更一般而言，如何使用引用来指导类型检查器？

（我知道我可以通过定义Choose为GADT 来解决此问题，我专门针对类型系列）

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module PropositionalDisequality where

import Data.Type.Equality
import Data.Void

type family Choose x y where
  Choose x x = 1
  Choose x _ = 2

lem :: (x :~: y -> Void) -> Choose x y :~: 2
lem refutation = _