我最近开始学习Isabelle，但我找不到一个非常重要的问题的答案:人们如何才能一步一步地推理Isabelle找到的“证明”？当然，我了解了Isar的“证明”，但1.这样的Isar证明并不总是能被Sledgehammer找到，2.即使Isar证明也不总是给出一步一步的推理。例如，我的一个定理的Isar证明是由Sledgehammer生成的，如下所示： have "... here is my formula ...."现
浏览 3提问于2015-06-07得票数 9
1回答
精益提高证据的可测量性吗？
、、、、
通过证据-可测量性，我理解人类用户可以“跟踪”证据的所有细节这一事实。有些事情是很难追踪的。例如，SMT证明是基于特定的启发式，然后被转换到验证程序中。在这种情况下，有一个简单的机制(不需要是专家就可以使用它们)来扫描证据失败的原因或检查证明程序的内部结构可能是有用的。
我在想，与Coq或Isabelle相比，Lean是否增强了这种证据的可测量性。
浏览 5提问于2020-08-30得票数 2
2回答
我一直在努力学习如何利用2016年伊莎贝尔。虽然原则上我喜欢异步验证检查的想法，但我不喜欢Isabelle/jEdit，原因很多，其中最严重的原因是它占用了太多内存(对我来说)。我将变量isa-isabelle-command设置为指向伊莎贝尔分发目录下的文件bin/isabelle。当我使用C-g的菜单启动Isabelle时，Emacs会挂起，当我通过C-g中断它时，我会在*isabelle*缓冲区中得到以下内容。val it = (): unit
浏览 8提问于2016-02-21得票数 6
回答已采纳
1回答
真的是这样吗？如果是这样的话，根据Isabelle的说法，我的证明真的有效吗？一般来说，我已经注意到，如果我在脚本中编写任何东西来代替"blast“，那么Isabelle将在输出中声明相同的内容，除了它可能还会在底部以红色表示存在一些失败。即使如此，如果我后来写"qed“，Isabelle似乎接受了证明的引理。这里发生什么事情？我如何确切知道我的证明何时被认为是
浏览 21提问于2019-01-12得票数 1
回答已采纳
我有一个证明by eval有点慢，我想优化代码。为了不那么盲目地这样做，如果jEdit可以显示它做by eval证明所花费的时间，那就太好了。
在Isabelle 2013中，这是可能的吗？
浏览 0提问于2013-05-02得票数 1
回答已采纳
是否可以获得在Isabelle中可以使用的所有谓词和函数的列表？
因为它经常发生，我开始手动定义一个谓词，我需要一个证明(如coprime)才能意识到它已经存在。
浏览 1提问于2017-02-17得票数 1
1回答
如何在伊莎贝尔身上写大楔子
、、、、
我想利用伊莎贝尔来做自动证明。但是，我在Isabelle中指定公式时遇到了问题。例如，我有这样的公式
其结果是“内部词汇错误⌂未能解析”。你能解释一下这里出了什么问题吗？非常感谢。
浏览 3提问于2020-10-07得票数 0
回答已采纳
1回答
我正在试着学习使用Isabelle/HOL。我想，“嘿，由一些开发它的人写的教程会很棒”，所以看了看，它的发布日期是2018年8月15日。然而，在尝试通过示例工作时，我在文本中发现了类似以下内容：如果发生任何奇怪的情况，我们建议您要求Isabelle通过Proof General菜单项Isabelle > Settings > Sh
浏览 11提问于2018-12-14得票数 0
回答已采纳
2回答
当用户试图证明auto或sledgehammer没有立即证明的东西时，是否有一种“通用”的非正式算法可供Isabelle用户遵循？一种通用的方法，用于计算auto是否需要用户制定的额外引理才能成功，或者如果更好，则使用其他证明方法。
一个相关的问题是:是否可以在某个地方找到一个表，其中包含所有证明方法以及应用它们的上下文？当我通读时，各种方法(一些方法的变体，如auto的许多变体)的描述散落在文本中，这使我经常在文本和Isabelle
浏览 4提问于2017-02-19得票数 6
我的问题是关于伊莎贝尔定理证明程序。我应该在编程模式下自编一个带有.thy后缀的理论文件，然后在验证模式下运行它以获得正确性的证明吗？我是否应该分别对这些代码进行编码以证明模型转换的正确性？
浏览 3提问于2020-05-30得票数 0
回答已采纳
在Isabelle/HOL中构造证明时，我们实际上是在构造一个lambda表达式，该表达式的类型与我们试图证明的理论相对应。
有没有办法看到与已证明的定理相对应的原始lambda表达式？
浏览 6提问于2020-07-30得票数 0
回答已采纳
我只想用命题逻辑(如notI、notE、impI、impE)中的基本自然演绎规则(ND)将这一证明转化为ab练习(供我学习)。等)。我可以很容易地在应用脚本中做到这一点： apply (rule impI) (* A ⟹ A ∨ B *) apply (rule disjI1) (* A ⟹ A *)但我试图证明Isar失败了：
浏览 2提问于2020-05-12得票数 1
回答已采纳
我在Isabelle src/HOL中复制了一个理论文件Test_Func.thy，它定义了函数add_123： theory Test_Funcbegin
fun没有关于未定义函数或不可见函数的错误信息，但是当函数定义和关于它的引理被分成两个文件时，这种简单的证明不知何故不起作用。我在伊莎贝尔2021年的jEdit中观察到了这一点，但在不同的背景下，我可以看到同样的事情也发生在伊莎贝尔2020中。
浏览 10提问于2021-05-06得票数 0
回答已采纳
我研究了Isabelle教程，它提供了一个示例，说明了它在验证安全协议中的作用。然而，这是有点超出我的理解，因为我只知道基础。我正在寻找一些例子，它们不仅是简单的定理，而且是使用Isabelle/HOL的实际应用。例如，证明一些算法或可能是验证性质系统或一些非平凡的数学定理。在任何地方都有这样的例子吗？我已经查看了伊莎贝尔官方页面中提供的所有应用程序的列表，但其中大多数都是定理的证明。
我也在看一个使用合金进行文件系统验证的例子。它提供了一个可以验证文件&#x
浏览 3提问于2015-05-21得票数 1
回答已采纳
在将证明语句键入到Isabelle (2020)理论文件中时，例如， from ‹prime p › have p: "1 < p " 当我输入一个引号时，jEdit界面应用程序会弹出一个工具提示，提示我插入一个打开的正如您在上面的代码行中所看到的，我一直在允许这样做，而且它似乎是被允许的。Isabelle文档似乎将内部语法视为嵌入的类别，这似乎允许使用引号或cartouche封装\<open ...\<close>.进行描述
浏览 18提问于2021-01-21得票数 1
回答已采纳
1回答
我试图将模式输入到Isabelle中，但是，当我在定理证明器中添加范围限制或域限制时，它不想解析。我在LaTeX中有以下模式：members: \power PERSON \\stockLevelstockLevel \\\
浏览 3提问于2016-02-08得票数 0
回答已采纳
偶尔也会有一个引理，其中try0崩溃了Isabelle/JEdit。那么，只有进程id上的kill -9才能工作。(我做了一些谷歌搜索，但找不到任何相关信息。)
浏览 1提问于2014-02-21得票数 0
回答已采纳
我在和方面都是新手。我试图在“证明通用”中设置一个与伊莎贝尔一起使用的黑色主题，但无论我选择什么主题(例如tango-dark、ample、monokai等)，未触及的内部语法都会以非常难以阅读的绿色突出显示。是否有一个很好的黑色主题可以很好地与Isabelle一起工作，或者我如何在Proof General中自定义Isabelle内部语法的突出显示？
浏览 5提问于2015-02-20得票数 0
3回答
(rule gcd_greatest) thus False by arith但是，当我将此文本复制到Isabelle实例中时，每行左侧都有多个“请勿输入”符号。其中一个写着“命令的非法应用”定理“在顶层”，所以我假设你不能简单地在顶层定义一个定理，并且维基百科的页面没有提供一个完整的初始示例。lexical error at: ℚ
Failed to parse proposition
浏览 4提问于2014-07-31得票数 3
云服务器
ICP备案
腾讯会议
云直播
对象存储
腾讯云开发者
