回答情况：
提问时间：
问题标签：
大约2-3周前，我开始学习定理证明者Isabelle。我仍然是一个绝对的初学者，到目前为止，我使用了教程“在Isabelle/HOL中编程和证明”。
到目前为止，我找到的关于矩阵的唯一帮助是查看。在Isabelle中是否有关于使用矩阵的教程或基本/中级示例？
浏览 3提问于2013-05-27得票数 2
回答已采纳
我想使用从Scala调用Isabelle。但是，在默认情况下(即使用中描述的调用)，libisabelle将下载一个新的Isabelle安装。val path = "/opt/Isabelle2016-1"我不知道这是否是我应该做的
浏览 6提问于2017-07-08得票数 1
回答已采纳
我想在Isabelle中创建一个函数F，它给出了一个公式 formula = pr int | neg formula | imp formula formula 如果公式是重言式，则产生我发现理解Isabelle的文档真的很难，而且我找不到这样的函数(我认为它应该已经存在)。
浏览 35提问于2019-12-16得票数 1
我看到的大多数Isabelle文档都说Proof-General支持Isabelle，但据我所知，PG在大约5年前就放弃了支持。 是否有其他可能将(当前的) Isabelle与Emacs一起使用？
浏览 28提问于2021-08-02得票数 2
回答已采纳
虽然原则上我喜欢异步验证检查的想法，但我不喜欢Isabelle/jEdit，原因很多，其中最严重的原因是它占用了太多内存(对我来说)。
如果我能和2016年伊莎贝尔一起使用好的老证据将军，那就太好了。我将变量isa-isabelle-command设置为指向伊莎贝尔分发目录下的文件bin/isabelle。当我使用C-g的菜单启动Isabelle时，Emacs会挂起，当我通过C-g中断它时，我会在*isabelle*缓冲区中得到以下内容。
浏览 8修改于2016-02-23得票数 6
回答已采纳
我安装了Isabelle2015并运行了Isabelle2015/Isabelle2015。$ ./isabelle tptp_isabelle 10 foo.tptp/home/asr/.isabelle/Isa
浏览 0提问于2016-01-29得票数 1
回答已采纳
我可以看到两种可能性：
有主要的Isabelle2021.exe，但是它启动了jEdit窗口，我仔细地检查了打包的jEdit选项，我没有发现jEdit可能作为输入伊莎贝尔命令行命令的工具。在bin目录中有3个脚本-- isabelle、isabelle_java、isabelle_scala_script，我为每个脚本复制了*.bat文件，并且尝试从Windows命令行运行，但我得到了：C:\Homes\Isabelle2021\Isabelle2021\bin>isabe
浏览 0提问于2021-03-21得票数 0
回答已采纳
我在Isabelle中有性能问题(也就是最新版本Isabelle2013-2)。我使用基于新接口的Isabelle/JEdit，。硬件：
最近的CPU，它是一个英特尔i7四核(移动实验室芯片)，16 it内存，快速的SSD硬盘。
浏览 1提问于2014-01-12得票数 2
我预计会有这样的命令："isabelle theory_file.thy"，但是在运行了Isabelle系统手册之后，我觉得一切都比这个复杂得多，最终就迷路了。因此，我有一个理论文件，并正在寻找一种方式，开始一个证明进程，包括Cygwin终端包括在Isabelle2016发行版的Windows。
我需要寻求的每一条建议或方向都受到高度赞赏。提前谢谢。
浏览 1提问于2016-09-28得票数 1
回答已采纳
我想看看Isabelle/HOL分布的向量空间理论文件中的定义。Isabelle邮件列表的This thread解释了如何使用命令isabelle make HOL-Base执行此操作。
浏览 41提问于2019-03-07得票数 2
回答已采纳
我正在尝试实现一个命令行版本的Isabelle/JEdit，这样我就可以
$ isabelle server # On another machine/terminal
OK [
浏览 3提问于2021-01-16得票数 2
我正在阅读"Programming and Provin in Isabelle/HOL“的介绍，并尝试做练习2.2。
浏览 25提问于2020-07-06得票数 1
回答已采纳
我看过一些文章，描述了如何使用工具HOL-Z和ZETA在Isabelle/HOL中使用Z符号。我找不到这些工具，它们曾经发布过吗？有没有其他方法可以将Isabelle与Z符号一起使用？
浏览 19提问于2021-11-01得票数 1
我正在学习如何用Isabelle编写ML代码(刚刚开始)。term_of和prop_of函数不能再使用了？
浏览 0提问于2017-11-01得票数 1
回答已采纳
按照和另一个建议，我为名义的伊莎贝尔创建了一个图像：堆映像在~/..isabelle下面创建：然后我开始
isabelle
浏览 0修改于2017-05-23得票数 4
回答已采纳
我在标准位置创建了一个Nominal2堆映像：我不能在理论面板中选择它来加载。/bin/bash
但是我什么都没做，或者，让
浏览 2修改于2017-05-23得票数 1
回答已采纳
在学习Isabelle (2020)时，我试图将文档中的一个示例复制到一个包含迭代含义的.thy文件中。由于文档是PDF格式的，我不知道它的正确ASCII应该是什么。我能得到的最接近的结果是： lemma "[[ xs @ ys = ys @ xs ; length xs = length ys]] ==> xs = ys" 但是Isabelle抱怨“内部语法错误，但Isabelle似乎将其视为一个列表，并抱怨列表和bool之间的冲突。 如何在ASCII中键入公式？ 一般来说，如何从PDF文档中找到表示法的AS
浏览 15提问于2021-01-05得票数 0
回答已采纳
我很抱歉最近问了这么多伊莎贝尔的问题。现在我有一个类型的问题。type_synonym my_fun = "nat ⇒ real"fixes n :: natand A :: "nat set"但是，在我的用例中，函数f的输出始终是集合{0..n}中的自然数。我想把这作为一个条件(或者有更好的方法来做呢？)我发现的唯一方法是：
assumes "
浏览 3提问于2020-01-27得票数 1
回答已采纳
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号