2回答
证明定理时的循环
、、、
在使用Debruijn指数和Coq中的替换将lambda演算形式化后，我试图证明以下定理。这些是表达式和beta约化的定义 Inductive expression : Type := | Abstraction (e : expression)当我试图证明这个定理时，我陷入了循环。 Proof. - intros. inversion H.然而，当我达到第三个子目
浏览 37提问于2021-04-02得票数 0
1回答
我有一个定理，在这个定理中，我证明了存在一个满足某些性质的对象。我通过构造对象证明了这个定理。然后，在另一个证明中，我想在第二个定理的陈述中引用第一个定理中定义的对象。我知道如果我用Defined而不是Qed关闭我的证明，对象应该是可访问的，但我不知道如何访问它。例如：
定理T1:存在x，P x。证明。..。已
浏览 2提问于2012-05-28得票数 2
回答已采纳
4回答
因为这些指令是邪恶的。就我个人而言，我不认为这个定理是错误的，但我认为它在现实世界中的适用性并不总是更好的选择。所以我做了一个小小的搜索，这些都是我的怀疑：
这个定理已经在流程图的结构上得到了证明，但它真的适用于计算机程序吗？定理的结果证明了每
浏览 4提问于2016-10-30得票数 5
回答已采纳
G是一个大素数阶的乘法循环群，g是G的生成元。定理1:给定g^{b^{-1}}和ab，很难计算a或b，在Z_p中随机选择a和b
定理2:很难区分以下分布：(g^{b^{-1}},ab)和(g^{b^{-1}},z)，其中a、b和z是在Z_p中随机选择的有证据证明这两个定理成立或不成立吗？
浏览 0提问于2020-07-13得票数 1
1回答
我要证明两对TR型的下列定理：
Definition p:= nat.到目前为止，这个定理的证明开始于引进毁灭定理，但我不知道证明这个定理的最佳策略。知道我该怎么证明这个定理吗？谢谢
浏览 0提问于2017-11-27得票数 2
回答已采纳
在学习的第三章时，我的导师提到了其中的一些函数是使用智能构造器模式构建的，并指出这种模式对定理的证明是有益的。那么，在Isabelle中什么是智能构造器模式，它如何帮助定理的证明？也许
浏览 0提问于2018-10-23得票数 1
回答已采纳
我的问题是关于伊莎贝尔定理证明程序。我应该在编程模式下自编一个带有.thy后缀的理论文件，然后在验证模式下运行它以获得正确性的证明吗？伊莎贝尔有许多编码字段，如数据类型、常数、函数、定义
浏览 3提问于2020-05-30得票数 0
回答已采纳
1回答
如您所知，要定义一个新类型的系统，一种方法是我们需要：
nat n ::= 0 | S n n nat
_____ Zero _______Succ
浏览 3提问于2014-06-03得票数 0
1回答
姚的定理说，对于一个分布，下一点不可预测性等同于伪随机.这链证明了姚定理，但证明依赖于非一致概率多项式时间算法.有证据证明姚的定理，而只使用统一的概率多项式时间算法？
浏览 0提问于2021-01-29得票数 2
回答已采纳
L语言的一个单定理自适应非交互式零知识证明(P，V)是一个满足条件的证明系统。零知识:在输入$x上有一个模拟器M\在L$中，输出与协议输出在计算上无法区分的集合。由于$x$是自适应的，所以它是基于公共引用字符串选择的。
单根定理意味着用一个公共的</
浏览 0提问于2018-03-23得票数 3
回答已采纳
我试图在coq中证明(~Q -> ~P) -> (P-> Q)，这是反正定理(P -> Q) (~Q -> ~P)的逆。目前我正在考虑使用同样的逻辑来证明反正定理，如下所示：
不展开。介绍A。B。C。也许我需要额外的公理来证明反正定理的逆。有谁可以帮我？
浏览 40提问于2021-05-12得票数 0
回答已采纳
我试图证明一个关于Prop的替换定理，但我失败得很痛苦。下面的定理能在coq中被证明吗?如果不能，为什么不能。重点是，在逻辑上，证明是通过归纳的。据我所知，Prop不是归纳定义的。如何在Coq中证明这样的定理？
浏览 2提问于2012-06-17得票数 7
我被一个定理困住了，我认为它是不可证明的。你能证明它或解释为什么它是不可证明的吗？这是由于G del的不完全定理吗？
浏览 0提问于2018-06-17得票数 0
回答已采纳
1回答
我在试着证明eqb_neq x =? y = false <-> x <> y.这是我当前的证明状态：
在证明过程中，我到达了最后一步，我只需要证明额外的辅助定理： n <> m我尝试了多种策略，但现在我甚至不确定是否可以证明这个辅助<em
浏览 18提问于2020-05-27得票数 0
回答已采纳
3回答
如果我正确理解Curry-Howard同构，每个依赖类型都对应一个定理，实现它的程序就是一个证明。这意味着任何数学问题，比如a^n + b^n = c^n，都可以以某种方式表示为一个类型。现在，假设我想设计一个生成随机类型(定理)的游戏，玩家必须尝试实现这些类型(定理)的程序(证明)。有可能控制这些定理的难度吗？也就是说，简单模式会产生琐碎的定理，而困难模式会产生更难的</
浏览 5提问于2016-04-21得票数 6
当我读教堂罗瑟第二定理时
如果有一个终止的减少，那么最外面的减少也将终止。我在想:是否有什么定理加强了丘奇罗瑟第二定理，使它讲述的是渐近时间复杂性而不是终结？
或者，是否可以证明按需要呼叫策略在所有减少策略中具有最小的渐近时间复杂度？
浏览 3提问于2017-02-22得票数 11
回答已采纳
在不指定Theorem定义的情况下，在Coq中进行交互式定理证明的最佳方法是什么？我想陈述一些初始假设和定义，然后交互式地探索转换，看看我是否可以在事先不知道的情况下证明任何有趣的定理。我希望Coq能帮助我跟踪转换后的假设，并检查我的重写是否有效，就像在交互模式下证明显式定理一样。Coq是否支持此用例？
浏览 3提问于2018-03-30得票数 2
1回答
我知道如何使用主定理，但不理解它的证明或直观的解释，特别是我不知道epsilon值是从哪里来的
我正在学习CLRS第三版，第97页。为了这个证明和扩展主定理的证明，还会有其他的资源/书籍吗？
浏览 10提问于2022-12-01得票数 0
回答已采纳
1回答
我是定理证明和伊莎贝尔的新手。我试图证明一个简单的(？)关于列表的伊莎贝尔定理。shows "list_difference somelist (modify somelist 0) <= 1"doneapply(
浏览 2提问于2014-10-31得票数 1
回答已采纳
1回答
我们被要求证明Parseval定理适用于任何输入图像。这是我的工作：import numpy as npspace = np.sum(np.abs(f)**2)print(space)这些值似乎不像预期的那样匹配我尝试
浏览 2提问于2021-02-03得票数 0
云服务器
ICP备案
对象存储
实时音视频
云直播
腾讯云开发者
