我正在尝试使用apply方法在Isabelle中使用一组有限的规则来证明一个引理。这组规则包含(P --> Q) = (\<not> P \/ Q)的disj_not1。这里是我使用我的规则disj_not1的地方’。但不幸的是，disj_not1是一个'if and only if‘规则，而不是'if’规则，并且<
浏览 9提问于2016-07-18得票数 1
回答已采纳
我在Isabelle中遇到了一个使用规则classical的自然演绎我更习惯于使用“排中律”(excluded_middle)和“反证法”(ccontr)我假设classical等同于上面的两个，但是我不能证明它们中的任何一个，也不能证明问题集中的lemma "A −→ ¬ ¬ A"。我不认为我只是误解了规则，因为我成功地<e
浏览 2提问于2016-07-14得票数 3
回答已采纳
在Isabelle中，我可以使用arbitrary关键字来概括归纳证明中的变量。这无疑适用于普通的归纳，比如在apply (induction n arbitrary: m)中。我也可以进行规则归纳，比如在apply (induction rule: R.induct)中。但是，在使用规则归纳时，如何泛化变量呢？在我的特殊用例中
浏览 0提问于2017-11-22得票数 0
回答已采纳
我很困惑于证明在伊莎贝尔。很明显你可以但我怎么能用规则来证明这一点呢？
或者，是否有一种方法可以转储simp使用的规则？谢谢。
浏览 0提问于2013-11-28得票数 4
回答已采纳
1回答
当Z3中的一个公式未满足并指定了(get-proof)时，会有一个输出，我找不到任何关于它是什么的信息。我在哪里可以找到关于这方面的任何文档？
在我看来很难读，有没有什么工具可以把这个作为输入呢？
浏览 5提问于2012-02-02得票数 6
回答已采纳
Isabelle需要很多时间来证明(在我看来)相当简单的数据类型转换函数的正确性。作为示例，我创建了数据类型来表示数学表达式和布尔表达式，并创建了一个函数来简化这样的表达式。(Or True b) = True" |by pat_completeness auto
termination by lexicographic_order 在我的笔记本上，Isabelle花了相当多的时间来证明
浏览 22提问于2019-05-24得票数 1
回答已采纳
在我学习Isabelle/HOL语法的练习中，我试图证明下面的一个玩具引理。它是关于lambda表达式(以及像“最伟大的”符号这样的以谓词作为输入的符号)。thesis qed 但是，上面的证明在auto或simp中都不起作用，并生成一条消息。Suc 0 = (GREATEST x. x ≤ Suc 0) 有没有人能解释一下这句话出了什么问题，或者如何证明这一点是正确的(如果这句话是正确的)？
浏览 24提问于2021-01-13得票数 0
回答已采纳
我在Isabelle src/HOL中复制了一个理论文件Test_Func.thy，它定义了函数add_123： theory Test_Funcbegin
begin apply(simp)
end 奇怪的是，使用没有关于未定义函数或不可见函数的错误信息，但是当函数定义和关于它的引理被分成两
浏览 10提问于2021-05-06得票数 0
回答已采纳
1回答
大约2-3周前，我开始学习定理证明者Isabelle。我仍然是一个绝对的初学者，到目前为止，我使用了教程“在Isabelle/HOL中编程和证明”。
到目前为止，我找到的关于矩阵的唯一帮助是查看。现在我想学习如何证明矩阵的性质。矩阵的lambda语法对我来说还是个新鲜事。在Isabelle中是否有关于使用矩阵的教程或基本/中级示例？
浏览 3提问于2013-05-27得票数 2
回答已采纳
我只想用命题逻辑(如notI、notE、impI、impE)中的基本自然演绎规则(ND)将这一证明转化为ab练习(供我学习)。等)。我可以很容易地在应用脚本中做到这一点： apply (rule impI) (* A ⟹ A ∨ B *) apply (rule disjI1) (* A ⟹ A *)但我试图证明Isar失败了：
浏览 2提问于2020-05-12得票数 1
回答已采纳
2回答
我如何在Isabelle中证明简单的lemma cd : "card {m∈ℕ. m <4} = 4"语句？auto对我没有帮助，奇怪的是sledgehammer超时了(即使我在右边使用了不同的值，比如3或5，以确保我没有忽略一些技术上的Isabelle细节，这些细节实际上可能会使基数计算为这些数字之一)。我的印象是，我必须使用一些引理(或从Set_Interval.thy中获得灵感)，因为这些类型的集合被广
浏览 0提问于2017-02-19得票数 1
我想知道在Isabelle/jEdit中有没有办法中止校样？ 我搜索了“重置”、“中止”等命令，但没有找到。 我知道有Sorry。但我不确定如果使用Sorry，手边的定理就会被假设为真或被放弃。目前，我注释掉了我无法证明的定理。但是它需要大量的输入(在(* *)中每个四个字符)来注释或取消注释一些东西，这是一种麻烦。 那么，在Isabelle中有没有一种标准/通用的方法来中止证明
浏览 15提问于2021-01-14得票数 0
回答已采纳
2回答
我一直在努力学习如何利用2016年伊莎贝尔。虽然原则上我喜欢异步验证检查的想法，但我不喜欢Isabelle/jEdit，原因很多，其中最严重的原因是它占用了太多内存(对我来说)。如果我能和2016年伊莎贝尔一起使用好的老证据将军，那就太好了。我将变量isa-isabelle-command设置为指向伊莎贝尔分发目录下的文件bin/isabelle。当我使用C-g的菜单启动Isabelle时，Emacs会挂起，当我通过C-g中断它时，我会在*i
浏览 8提问于2016-02-21得票数 6
回答已采纳
我从Isabelle/HOL开始，学习发行版中包含的prog-prove.pdf教程。我在4.4.5节“规则倒置”中遇到了困难。但是现在我想用同样的证明方法，把同样的事实和引理说出来，这是行不通的：proof cases (* ... *)
伊莎贝尔在ev0停留，
浏览 0提问于2015-07-04得票数 3
回答已采纳
我注意到，在使用Isabelle/HOL Isar时，有几种方法可以处理通用量化。我正在尝试以一种适合本科生理解和复制的风格来编写一些证明(这就是我使用Isar的原因！)例如，在Coq中，我可以编写forall x, P(x)，然后我可能会说“归纳x”，这将根据相应的归纳原理自动生成目标。然而，在Isabelle/HOL Isar中，如果我想直接应用归纳法原理，我必须在没有任何量
浏览 0提问于2015-12-28得票数 7
在Isabelle/HOL中构造证明时，我们实际上是在构造一个lambda表达式，该表达式的类型与我们试图证明的理论相对应。
有没有办法看到与已证明的定理相对应的原始lambda表达式？
浏览 6提问于2020-07-30得票数 0
回答已采纳
我最近开始学习Isabelle，但我找不到一个非常重要的问题的答案:人们如何才能一步一步地推理Isabelle找到的“证明”？当然，我了解了Isar的“证明”，但1.这样的Isar证明并不总是能被Sledgehammer找到，2.即使Isar证明也不总是给出一步一步的推理。例如，我的一个定理的Isar证明是由Sledgehammer生成的，如下所示： have "... here is my formula ...."现
浏览 3提问于2015-06-07得票数 9
1回答
我经常发现，“auto”并不能解决一个对我来说很简单的方程，至少对涉及∪、∩和-的术语进行一些搜索。goal (1 subgoal): ArityAnalysis.Afix Aexp Γ⋅(Aexp e⋅n) f|` ((fv Γ ∪ fv e - domA Γ) ∩ - domA Γ)
我可以绕过它(例如by auto (metis Diff_eq Diff_idemp))，但我想知道是否存在
浏览 2提问于2014-07-10得票数 1
回答已采纳
2回答
在证明语句时，Isabelle是否支持自定义大小写区分？假设我想证明一个关于所有自然数n的声明，但证明完全不同，这取决于n是偶数还是奇数。是否可以在证明中进行大小写区分，例如 assume "n mod 2 = 0" next assume "n mod 2 = 1"<proof>到目前为止，我将引理/
浏览 13提问于2018-01-26得票数 4
回答已采纳
云服务器
ICP备案
云直播
腾讯会议
实时音视频
腾讯云开发者
