腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(27)
视频
沙龙
1
回答
如
何在
精
益
定理
证明器
中
证明
数学
归纳
公式
?
theorem-proving
、
lean
谁能帮助我理解如何写一个简单的结果的
证明
,可以很容易地通过
归纳
法获得,例如第一个n自然数的和的
公式
:1+2+...+n = n(n+1)/2,使用瘦
定理
证明器
?
浏览 10
提问于2020-01-05
得票数 1
回答已采纳
2
回答
精
益
中
整数的
归纳
创建非int类型。
types
、
type-conversion
、
induction
、
lean
我想在整数变量上使用
归纳
法,在正方向和负方向进行
归纳
步骤。考虑以下
定理
(为了
证明
,无论是否有意义):begin -- inductive stepscase int.of_nat⊢ int.of_nat x = 5 x: ℕ合理地,
归纳
产生了两种情况但同样发生的是,x现在已经成
浏览 2
提问于2021-07-31
得票数 1
回答已采纳
1
回答
精
益高尔夫:帕斯卡对斐波纳契
code-golf
、
math
、
combinatorics
、
fibonacci
、
lean
Pascal三角形和Fibonacci序列有一个有趣的联系:来源:
数学
是有趣的-帕斯卡三角 = n.succ.fib :=由于语句本身依赖于当前版本的mathlib,因此鼓励您使用
精
益
网页编辑器(而不是TIO)来
证明
您
浏览 0
提问于2021-10-08
得票数 20
2
回答
定理
证明器
中
的
归纳
证明
(Z3,吸血鬼,带有TPTP语法)
logic
、
z3
、
smt
、
theorem-proving
、
logic-programming
我正在测试一些
定理
证明器
的
归纳
能力(
如
Z3,Alt,吸血鬼等)。使用TPTP语法。令我惊讶的是,他们
中
没有一个人成功地
证明
了以下简单的猜想: !CPU = 60.09 WC = 35.47 这个猜想可以很容易地通过
归纳
浏览 20
提问于2022-04-20
得票数 1
回答已采纳
1
回答
瘦,f,和dafny有什么区别?
dafny
、
lean
、
fstar
他们来自微软,看起来像是证据助理?除了句法上的差异,是否有一些实际的方面使它们彼此不同(比如自动化能力、表达能力等)?我是正式核查的新手。
浏览 1
提问于2017-09-02
得票数 21
2
回答
如果Z3不支持诱导,Dafny是如何支持的?
z3
、
proof
、
dafny
、
formal-verification
、
induction
而且,据我所知,每当我们在Dafny中使用断言时,在它下面发生了什么,它构造了
证明
义务,然后使用Z3对它们进行计算。然而,我读到Z3不支持
归纳
:例如.然而,任何非平凡的属性都需要通过
归纳
法来
证明
.Z3目前不支持
归纳
证明
.() 因此,我的问题是:每当我们设置{:induction true}时,如果不使用Z3,在Dafny
中
如何执行这种
归纳
?
浏览 39
提问于2022-09-26
得票数 1
回答已采纳
1
回答
Z3与coq的区别
z3
、
coq
、
theorem-proving
在我看来,coq是一个
证明
助手,因为它要求用户填写
证明
步骤,而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略?或者可能coq
中
的
证明
搜索能力没有Z3那么强大?
浏览 1
提问于2012-07-18
得票数 44
回答已采纳
2
回答
如何执行
证明
助理?
coq
、
isabelle
、
proof
举证助理的主要任务是什么?对于编译器,有一个与我类似的问题:
浏览 3
提问于2019-11-06
得票数 3
回答已采纳
1
回答
精
益高尔夫:列表游戏Lv2 (is_in_append,is_in_rev)
code-golf
、
lean
标题是对自然数博弈的敬意,这是一个很好的交互式教程,用来
证明
精
益
中
自然数的某些特性。现在它从import tactic开始,这意味着您可以自由地使用强大的
数学
库战术。 我注意到我可以在没有问题的情况下定义一般的列表表示法[a, b, ..., z]。在
证明
上进行
归纳
。它的工作原理类似于nat或列表上的
归纳
:要
证明
一个∀ (x:A) (l:list A), is_in
浏览 0
提问于2021-10-13
得票数 9
1
回答
将要操作的数据与
证明
操作是正确的
证明
解耦
coq
它不利于代码重用:我被迫重新定义通常的列表函数(
如
列表连接),并重新
证明
通常的列表
定理
(例如列表连接的相联性)。我想到了一种不同的方法,包括三个步骤:
归纳
taggedElement :=标记: t1 t2,element t1 t2 -> taggedElement将标记元素的有效列表定义为元组,其元素是标记元素的任意列表,并
证明
这些元素与相邻元素兼容。 (*我不知道如
何在
Coq
中
这样做,因此问题就来了!
浏览 4
提问于2012-09-11
得票数 3
回答已采纳
3
回答
证明
助理的经
证明
的计算
coq
、
isabelle
、
theorem-proving
、
proof-of-correctness
、
hol
是否有像Coq、Isabelle、HOL、Metamath等
证明
助手/检查人员被用来
证明
符号计算的正确性的例子?我特别感兴趣的是微积分和线性代数的例子,例如求解定积分或不定积分、微分方程和矩阵方程。更新:更具体的是,想知道是否有微积分和线性代数本科作业的例子可以正式解决(可能是在
证明
助手的帮助下),这样解决方案就可以由验证检查器自动验证。
精
益
的一个非常简单的例子是。
浏览 2
提问于2021-11-15
得票数 2
回答已采纳
1
回答
量化的列表长度限制导致unsat
z3
、
smt
通过下面的示例,我试图以量化的方式对所有可能的列表的长度设置一个限制。这将导致一个“非卫星”的结果,我相信这是正确的。我发现很有趣,但我的问题并没有得到真正的回答。此外,答案是旧的,并参考SMT-LIB版本2.0 (以及一个对一个未量化的版本)。也许Z3现在能够以一种我不知道的方式做到这一点。(set-option :produce-unsat-cores true) (declare-datatypes ((List 1)) ((par (T) ((con
浏览 1
提问于2021-01-21
得票数 0
回答已采纳
3
回答
等式传递的coq
归纳
法
coq
、
induction
我试图制定一个
归纳
原则,允许我这样做。下面是一个程序,用一个简化的例子替换了所有不必要的
定理
。目的是用allLE_countDown
证明
countDown_nth,并使list_nth_rect具有方便的形式。(这个
定理
很容易被直接
证明
,没有任何这些。)因此,我有list_nth_rect,并能够使用它和
精
化,通过引用第n个元素来
证明
定理
,
如
所需。然而,我不得不亲自构造P命题。通常情况下,你会喜欢使用感应。那么,如何才能改变
归
浏览 3
提问于2017-10-03
得票数 4
回答已采纳
1
回答
SMT求解者和正式验证者之间有什么区别?
formal-verification
、
smtchecker
这个问题成立。这两者有什么区别?在最小的可靠代码上使用这两个工具的示例是什么?
浏览 0
提问于2023-02-21
得票数 4
回答已采纳
4
回答
B-Jacopini
定理
algorithm
、
theory
、
theorem
根据B hm-Jacopini
定理
,只能用以下三种语句来编写算法: 就我个人而言,我不认为这个
定理
是错误的,但我认为它在现实世界
中
的适用性并不总是更好的选择。所以我做了一个小小的搜索,这些都是我的怀疑: 这个
定理
已经在流程图的结构上得到了
证明
,但它真的适用于计算机程序吗?
浏览 4
提问于2016-10-30
得票数 5
回答已采纳
1
回答
深入研究类型系统和类型理论
types
、
programming-languages
我想了解类型背后的实际理论,而不仅仅是了解一些现有语言中最新的实际变化(例如,不仅仅是Haskell或Scala的类型系统如何工作)。
浏览 0
提问于2012-06-16
得票数 35
回答已采纳
11
回答
函数式编程范式有没有可视化的建模语言或风格?
programming-languages
、
haskell
、
modeling
、
functional-programming
UML是一种标准,旨在对将用面向对象语言编写的软件进行建模,与Java并驾齐驱。尽管如此,它可能被用来对以函数式编程范型编写的软件进行建模吗?考虑到嵌入的可视元素,哪些图表将变得有用?编辑时间:2009年9月2日 我正在寻找的是代码中所发生的事情的最直观、最轻量级的表示。容易遵循图表,可视化模型不一定是针对其他程序员的。我很快就会用Haskell开发一个游戏,但是因为这个项目是为了我的毕业总结工作,所以我需要介绍所提出的解决方案的某种形式。我想知道是否有等同于UML+Java标准的标准,但对于Ha
浏览 4
提问于2009-09-01
得票数 43
回答已采纳
11
回答
有一本关于
数学
的规范书给程序员吗?
math
老实说,我
数学
不好。你能给我什么建议来提高我的
数学
技能,这样我就不会对我的程序员同伴那么缺乏安全感了?您可以推荐哪些步骤或指导方针来提高我的
数学
技能?有没有一本书是描述程序员
数学
方面的最佳实践、设计方法和其他有用信息的事实上的标准?那本书让它变得特别了吗?
浏览 0
提问于2011-06-20
得票数 51
25
回答
数学
和编程有什么关系?
development-process
、
math
现在,我们开始使用基本Java之类的(从底部您可能会说)--这很好,除了知道如
何在
Java中使用"Hello“之外,我没有编程经验。我很抱歉我的问题含糊不清,我刚开始对我作为一个暗号猴子学生所涉足的世界有一个大致的了解…
浏览 0
提问于2012-02-26
得票数 92
9
回答
教学系统分析和设计-需要多少编程经验?
oop
、
design-patterns
、
uml
我的问题有两个:你认为学生在接触这些主题之前需要多少编程经验(或者你认为他们应该在学习代码之前学习它们);第二,你认为在课程开始时,你觉得怎样才是公平和适当的方法来预先测试他们,因为他们的背景
中
没有一致的语言或平台
浏览 6
提问于2008-12-20
得票数 1
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
黎曼猜想被证明了!
十年来论文量激增,深度学习如何慢慢推开数学推理的门
被证明的黎曼猜想跟区块链加密算法有什么关系?
被证明的黎曼猜想跟区块链加密算法有什么关系
TPS及计算方法
热门
标签
更多标签
云服务器
即时通信 IM
ICP备案
对象存储
实时音视频
活动推荐
运营活动
广告
关闭
领券