proof 相关问题

数学证明是证明数学陈述真实性的任何数学论证。非正式证据通常以自然语言呈现，并以协商一致方式保持真实;形式证明通常以符号形式呈现，并且可以机械地检查。 “证据”可以有效或无效;只有前者才能构成实际证明，而后者通常指的是证明有缺陷的尝试。

我正在尝试使用Lean 4将停止问题简化为双曲几何，以证明双曲几何的不可判定性，遇到图灵机对角化的问题，a...

math proof turing-machines lean

回答 1 投票 0

我已经在 Coq 中实现了一篇论文的证明系统，如下所示。期限证明系统归纳术语：类型 := | VarTerm (v: Var) | PrivKeyTerm（k：名称） |公共密钥术语（k：名称） | PairTerm (t1 t2: T...

types logic coq proof

回答 1 投票 0

弗洛伊德算法检测链表证明中的循环

我在堆栈溢出内外的几篇文章中看到了弗洛伊德算法的几个证明。所有这些都证明了算法的第二部分，即为什么要找到

linked-list proof floyd-cycle-finding

回答 2 投票 0

用递归公式替换证明

以下问题和部分解决方案来自 Richard Bird 的 Thinking Functionly with Haskell (pp 132-133, 139) 给定折叠 f e (x:xs) = 折叠 f (f e x) xs 折叠 f e [] = e 证明折叠（@）...

haskell fold proof

回答 1 投票 0

lambda 演算中的加法证明

不明白add(m, n) = m + n证明中的这个转变：(λmn.λsz.m, s, (n, s, z)) = (λs.λz.sm(z )) , s, (λs.λz.sn(z)) 解释一下转换的逻辑（可能是 b-约简或者...

math addition proof lambda-calculus

回答 1 投票 0

数据结构的时间复杂度分析

我对插入或删除等数据结构基本操作的分析有点困惑。当我被问到创建一个支持删除操作的数据结构，或者插入O...

algorithm data-structures computer-science proof

回答 1 投票 0

Dafny 关于找零的简单证明不起作用

我想证明以下代码以 5 和 3 个钞票/硬币的形式返回给定金额（金钱）：函数 sum(ns: seq): nat { 如果|ns| == 0 那么 0 别的 ns[0] + 总和(ns[1..]) } 我...

algorithm proof dafny

回答 1 投票 0

Big Oh 表示法 O((log n)^k) = O(log n)?

用大 O 表示法是 O((log n)^k) = O(log n)，其中 k 是某个常数（例如对数 for 循环的数量），对吗？我的教授告诉我这个说法是正确的，但是他这么说......

big-o proof

回答 3 投票 0

WP插件：为什么下面的简化代码验证失败

我是一位新的 Frama-C 用户，我正在尝试证明一个大型项目的某些属性。我看到一个特定的证明失败了，并尝试将问题减少到最小的可重现示例，并且......

static-analysis verification proof frama-c formal-verification

回答 1 投票 0

Beamer 中的定理和证明环境

我目前正在尝试使用四开投影仪制作讲座幻灯片。我想在 beamer 中使用定理环境，但是 qmd 文件无法正确渲染。使用乳胶停止渲染...

latex proof beamer quarto theorem

回答 1 投票 0

函数 f 的正式定义：Q → Q

给出函数的正式定义 f : Q → Q 是单射但不是满射，或者证明为什么不存在这样的函数。

function math theory proof

回答 2 投票 0

证明 max x y = y 给定 x <= y in Idris 2?

我是 Idris2 的新手，需要一些指导来证明以下关系： Simply_max : (LTE x y) -> (max x y) = y simple_max prf = ?代码我在文档中读到，构造函数...

proof idris2

回答 1 投票 0

如何指示`auto`在证明搜索过程中简化目标？

我的问题的一个最小示例如下所示：目标让 x := x 中的 True。这个问题可以通过 simpl 立即解决。自动，但是自动。不起作用。在我的实际情况中，搜索树比...

coq proof

回答 1 投票 0

可以重命名 coq 术语吗？

抱歉，我不确定标题是否是适当的问题。我一直在学习逻辑基础。在引理“double_plus”中，我用这个解决方案解决了它：引理 double_plus : fo...

coq proof coq-tactic

回答 1 投票 0

如何从存在子句中提取变量

我试图用Dafny简单地简化为荒谬的证明，通常当我这样做时（在现实生活中的数学中）我使用诸如“好吧，现在让我们选择一个满足这个属性的p......

proof dafny

回答 1 投票 0

如何证明这个不变量？

我的目的是证明霍纳规则是正确的。为此，我将霍纳当前计算的值与“实”多项式的值进行比较。所以我写了这段代码：包...

ada proof invariants proof-of-correctness spark-ada

回答 1 投票 0

如何证明nat_to_bin结合了bin_to_nat b = Coq中标准化b

我是新手，用参考书软件基础入门学习Coq 在这句话的最后部分，有一个练习证明将二进制更改为自然数并且

coq proof

回答 1 投票 0

伊莎贝尔的反证法证明

我理解 ccontr 是如何工作的，但是我不确定如何（或者即使可能）在用假设声明的引理上使用它。举个简单的例子，一切都很好：引理l1：“A⊆B⟶A∩...

isabelle proof

回答 1 投票 0

根据定义对无限的 IO 操作列表进行排序是否会导致永无止境的操作？或者有什么办法可以摆脱吗？

这实际上是我想通过我之前的问题来理解的东西，但我用词不当，理所当然地认为解决方案必须以某种方式建立在顺序和重复的基础上，所以我得到了一个

haskell functional-programming language-lawyer proof io-monad

回答 1 投票 0

证明停止问题是NP困难的？

在回答有关 NP、NP-hard 和 NP-complete 定义的问题时，Jason 声称：停机问题是典型的 NP 难问题。这是给出

theory proof halting-problem np

回答 2 投票 0

proof 相关问题

最新问题