定理证明，目前是自动推理中最发达的子领域，是计算机程序证明数学定理。
为什么我不能在Isabelle中明确证明我的案件，但已经给出了证明，但给出了“未能完善任何待解决的目标”错误？
我正在学习具体语义的第5章。在研究此玩具示例证明时，我遇到了一些错误：引理显示为“¬ev（Suc 0）”，我知道这超出了需要（由于情况而定...）>
为什么不能在Isabelle中简化Σ{0} = 0以使它们相等？
[我正在阅读第5章（Isar），我尝试对“Σ{0..n :: nat} = n *（n + 1）div 2”做结构归纳证明，但失败了：引理“Σ{ 0..n :: nat} = n *（n + 1）div 2“证明（归纳n）显示...
如何在Isabelle证明中打印局部变量和主题（在Isabelle中调试）？
我有时很难使用Isabelle，因为我无法像普通编程中那样拥有“打印命令”。例如，我想看什么主题。具体的语义书说：未知的？...
我有时很难使用Isabelle，因为我无法像普通编程中那样拥有“打印命令”。例如，我想看什么主题。具体的语义书说：未知的？...
我在使用字符串可确定性时遇到麻烦。首先，我感到困惑，为什么在阿格达（Agda）中难以决定性工作，而在Coq中看起来却像黄油一样光滑。当我试图证明这一点...
我有一个函数减去两个Nats。我如何证明我要传递给它的第一个参数实际上小于第二个伪参数：（k：Nat）->（n：Nat）-> {自动更小：LTE kn}-＆...
可扩展性公理说，如果两个函数在域的每个自变量上的作用相等，则它们相等。公理func_ext_dep：forall（A：类型）（B：A->类型）（f g：forall x，B x），...
如何在字符串的布尔等式上进行模式匹配，并同时在Coq的证明中获得所需的命题等式？
我在尝试证明SF中的substi_correct定理时陷入困境，因为我不知道如何分解布尔相等性，同时又将其断言为命题相等性。定理...
为什么我们需要证明两个命题才能在Isabelle中应用析取消除？
[我看到了析取消除的证明规则，并且我注意到我们必须证明两个语句都可以使用它：？P∨QQ⟹（？P⟹R）⟹（？Q⟹R）⟹为什么那？就像在正常逻辑中，如果我知道一个...
我想阻止isabelle在编写时执行证明步骤，因为当我尝试使用rule_tac告诉它消失时该术语应该是什么时，它不可能记住复杂的方程式。 ...
我正在研究软件基础（第1卷：逻辑基础）的IndProp.v中以下定理Sn_le_Sm__n_le_m的证明。定理Sn_le_Sm__n_le_m：nm，S n≤S m→n≤m。证明。 ...
我已经在列表上定义了一个反向函数，并且我试图证明一个琐碎的属性，即空列表的反向是空的。应该通过反射来证明：def reverse（t：listα）：...
我正在尝试使用export_code工具进行以下定义：definition set_to_list ::“（''a×'a）set⇒（'a×'a）list”其中“ set_to_list A =（SOME L. set L = A）“这不起作用，因为...
它向我抱怨我有一个解析错误，但是我在手册中找不到应该是正确的语法... | “” my_function x b（Cons3 y）=如果x = y然后b else（Cons3 y）“错误：内部语法...
此证明是Avigad等人在“逻辑和证明”中基于策略的版本。 import data.nat.prime打开nat定理sqrt_two_irrational_V2 {a b：ℕ}（co：gcd a b = 1）：a ^ 2≠2 * b ^ 2：= ...
如何从LEAN的第一原理证明（（x，p x）→（∃x，p x）？
[基本原理的基本含义的证明，即“精益定理证明” 4.4中的练习，击败了我到目前为止的所有尝试：打开经典变量（α：类型）（pq：α→Prop）变量a：。 。
在LEAN教程的第3章末尾，我仍然在苦苦挣扎（因此阻止我进一步阅读本手册的两个证据是：定理T11：¬（p↔¬p）：= .. 。
[Imperial College开发的自然数游戏是一个很棒的主意，它对LEAN中的证据编写基础有很大帮助。在经历了大部分内容之后，仍然有一个“额外” ...