回答情况：
提问时间：
问题标签：
我看过一些文章，描述了如何使用工具HOL-Z和ZETA在Isabelle/HOL中使用Z符号。我找不到这些工具，它们曾经发布过吗？有没有其他方法可以将Isabelle与Z符号一起使用？
浏览 19提问于2021-11-01得票数 1
我在Isabelle/HOL中有一些定义和定理，并且需要在HOL中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有程序可以(半自动)执行这样的翻译？
浏览 17修改于2018-07-30得票数 6
我很抱歉最近问了这么多伊莎贝尔的问题。现在我有一个类型的问题。type_synonym my_fun = "nat ⇒ real"fixes n :: natand A :: "nat set"但是，在我的用例中，函数f的输出始终是集合{0..n}中的自然数。我想把这作为一个条件(或者有更好的方法来做呢？)我发现的唯一方法是：
assumes "
浏览 3提问于2020-01-27得票数 1
回答已采纳
从那时起，伊莎贝尔HOL不再启动，即使在重新安装之后(顺利通过)。错误消息如下：“启动错误:启动Java VM错误”。这发生在我测试的两个版本(2013年-2和2015年)。
浏览 0提问于2015-08-16得票数 0
回答已采纳
我在试着证明某种形式AFAIK结合定理是库的一部分，但没有被标记为简化，所以我需要手动添加它们。适当的theory的确切名称是什么/它们是在哪一个中定义的？
浏览 2提问于2016-11-15得票数 0
回答已采纳
我发现Isabelle/HOL中的许多定理更倾向于元级蕴涵：而不是对象逻辑层次，即高阶逻辑蕴涵。
说，粗略地说，应该使用元级含义来将假设与规则语句中的结论分开。什么时候和什么时候我应该使用HOL的含义？
浏览 7提问于2020-02-28得票数 4
回答已采纳
我正在为Isabelle2013/HOL寻找免费的、高质量的教程和文档(除了Google-ing和挖掘一点之后明显的那些教程和文档)。你能给我推荐一些吗？
浏览 6提问于2013-11-11得票数 2
回答已采纳
我试图通过封装用于证明目标absorptionRule的策略来创建一个名为“!(p:bool) (q:bool). (p==>q) ==> p ==> p /\ q”的定理。但是，我在ACCEPT_TAC上得到了一个例外。当我一个接一个地执行每一种战术时，一切都很好。TAC_PROOF( REPEAT STRIP_TAC THEN
ACCEPT_TAC(ASSUME ``p:bool``)
浏览 0修改于2018-05-08得票数 2
回答已采纳
我正在做一个证明，我能够将它简化为“of_int i=0 ==> i=0”。这看起来像是规则“of_int_eq__iff”的一个简单应用，但是我无法成功地应用这个规则。在进一步的研究中，我发现我无法证明下面的引理不管用什么方式。也就是说，除非我在context ring_char_0中声明了引理。然后，引理可以很容易地证明如下：lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
浏览 0提问于2014-11-01得票数 1
关于伊莎贝尔/霍尔，我有一个初学者的问题：lemma shows "{(x,y) . x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(x,x). x < n}"proof (prove) goal (1 subgoal): 1. {(x, y). x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(xa, x). x < n}
浏览 3提问于2020-01-05得票数 0
回答已采纳
有人能帮我用伊莎贝尔/霍尔中的下列方程(一阶逻辑)证明X=M吗？其中N, M, X是整数常量。n整数变量.
浏览 1修改于2019-09-23得票数 1
回答已采纳
我在伊莎贝尔/霍尔试图证明这个引理。但是nitpick找到了反例来证明这一点和它的否定这怎麽可能？我查看了未定义的定义是如何定义的，这是一个公理：但这仍然是经典逻辑，对吧？因此，无论是"(0::nat) = undefined"还是"(0::nat) ≠ undefined"都应该是真的。我有一个类型的函数：
type_synony
浏览 0修改于2020-01-20得票数 3
回答已采纳
我从Isabelle/HOL开始，学习发行版中包含的prog-prove.pdf教程。我在4.4.5节“规则倒置”中遇到了困难。
浏览 0提问于2015-07-04得票数 3
回答已采纳
问题我在寻找一个关于计划元级评估器的东西。我只对验证器感兴趣，而不是自动定理证明的策略。我想从零开始实现一个简单的验证器(纯粹出于教育原因，而不是用于生产)。我怀疑核心验证器算法非常简单(而且优雅)。但是，我找不到它。
浏览 3修改于2013-03-01得票数 8
我试图使用imports Complex_Main "~~/src/HOL/Analysis/Finite_Cartesian_Product"中的向量(vec)来说明它，但没有成功 如下所示： lemma
浏览 15提问于2021-01-22得票数 1
考虑以下简单过程语言的Isabelle/HOL定义：Get :: "['a channel, 'a ⇒ process] ⇒ process"
然而，这需要支持数据类型中的存在量化，而这是Isabelle/HOL
浏览 2提问于2018-07-19得票数 4
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号