问题标签 [induction]

我在完全理解如何证明以下某些陈述时遇到问题。

例如我有一个声明：n^2logn = O(n^2). 如果我错了，请纠正我，但这说明n^2是bigO. n^2logn意味着n^2增长速度比n^2logn. 现在我们将如何证明这一点？我假设我需要使用我曾尝试使用但陷入过程中的归纳证明。我可以将此语句重写为n^2logn <= n^2吗？

是否可以使用归纳法来反驳某些东西？例如，反驳n!=O(n^n). 或者通过简单地证明任意值（假设大于 2）不满足该陈述来反驳该陈述是否有效？

最后为了清楚起见，bigTheta 指出方程在正确增长时是等价的？

CS学生在逻辑课上苦苦挣扎。这个问题让我一头雾水

归纳定义字符串集

找到以下字符串集的归纳定义：

S = {apbcr | p 是自然数，r 是大于 0 的自然数} * p 和 r 是上标*

问题是“使用强归纳表明，2 个或更多偶数的任何总和都是偶数”。现在，我对常规归纳很好，但我迷失在强归纳的符号中。到目前为止，我有：

BASE：（我们将使用 2 作为偶数）

根据序列定义，n=2，A2 = 4（偶数）

根据序列定义，n=3，A3 = 6（偶数）

因此，我们有 P(2) 和 P(3)

我不知道从这里去哪里，如果有人能引导我朝着正确的方向前进，那就太好了

你将如何解释归纳谓词？它们是用来做什么的？他们背后的理论是什么？它们只存在于依赖类型系统中，还是存在于其他系统中？它们在某种程度上与 GADT 相关吗？为什么它们在 Coq 中默认为 true？

这是 Coq 的一个例子：

你会如何使用这个定义？它是数据类型还是命题？

不变量：就在第 3 行评估循环保护之前，删除了最右边的 d 位的 n 与 val 相同。（假设数字 0 需要 0 位来写出，并且是唯一需要 0 位来写出的数字）。

使用归纳法证明循环不变量成立。

现在我一直认为归纳证明是假设通过用 k 替换方程中的变量将是真的，那么我必须证明 k+1 也将是真的。但是在这个问题中我并没有真正给出方程式，而只是一段代码。这是我的基本情况：

就在第 3 行评估循环保护之前，d 等于 0，在第 2 行，val == n，因此如果 n 删除了最右边的 0 位，则为 val。因此，基本情况成立。

我不确定如何在此之后编写归纳步骤，因为我不确定如何证明 k+1 ..

所以我有这个问题，我正在研究关于上下文无关语法的归纳证明。

鉴于这个语法

S-> aSb | 不锈钢 | 抗体

使用归纳法证明文法生成的字符串不以abb开头。

很容易看出这实际上是正确的，但是我对如何对其进行正式证明有一些问题。

我正在考虑对单词的长度使用按值归纳的课程，或者对推导的长度使用按值归纳的课程（在这种情况下，我真的不知道哪个更好）。

让我们对推导的长度使用归纳法。

基本情况：推导的长度是一步，那么唯一的可能性是 S-> ab，这显然成立。

归纳假设：如果 S=>w' 有 n 个推导（n>0），则 w' 不以 abb 开头

感应步：？？？

归纳步骤是我遇到问题的地方，我真的不明白该怎么做。

我想知道是否有人可以解释我应该在那里做什么？

谢谢！

我只是在阅读这篇（http://condor.depaul.edu/ntomuro/courses/417/notes/lecture1.html）论文，它证明了 AVL 树中的最小节点数。但是，我不明白结果的含义，因为 O(log n) 根本不是指节点数。这怎么可能是证明？但是，我确实了解第一步以及如何简化迭代。但是在第四步之后，我无法理解他到底在做什么（尽管我可以模糊地想象）。谁能向我解释一下，最后几行证明了什么，以及他如何在第 1 部分末尾简化表达式？

谢谢

如您所知，要定义一个新的类型系统，一种方法是我们需要：

1. 语言语法
2. 打字规则

然后我们需要证明一些我们认为可以使用上述类型规则证明的定理。为了证明这些定理，一种方法是我们可以使用归纳法（Rule Induction）。

例如，我们有一个这样的系统：

我们定义了 2 个规则“Zero”和“Succ”，如下所示：

然后，我们提出一个定理，我们认为这个定理是正确的，我们需要证明它。

我们可以使用定义的规则轻松证明这个定理。这就是所谓的规则归纳。

那么有没有人知道可以帮助练习规则归纳的资源？

在一些使用缺失值数据的任务中，我必须使用 J48 树归纳算法。现在我将做一些经验研究，比较 J48 树归纳上下文中的不同缺失值方法，不同的 UCI 训练数据集和不同的人工这些数据集的截肢率（标准，+10%，+40% 截肢）。

我的主要问题是，我如何在 J48 源代码中实现以下方法，或者在我自己的代码中使用 Weka J48 类更好地实现。我可以将这种方法作为元分类器或其他方式处理吗？我想测试的方法与 J48 标准处理和随机森林相对应：

• 删除缺少属性的对象（完整案例）
• Hot-Deck-Methods（寻找内部捐赠者的概念）
• 代理拆分（使用其他属性进行拆分，例如 CART 处理缺失值）
• 使用其他决策树（概念->缺失属性值）进行插补以找到缺失的属性值

我必须停用集成的 J48(C4.5) 缺失值处理吗？我怎样才能停用这个？我认为 J48(C4.5) 将使用特殊值方法来查找测试、概率分布和在训练数据分区期间将对象拆分为部分，而在分类期间则使用其他方法。

现在其他所有人都可以轻松扩展J48的其他缺失值方法吗？

非常感谢！

这是自然数均匀性的归纳和计算定义。

以及一个暗示另一个的证明。

起初我并没有多想这个证据，但仔细一看，我发现了一些令人不安的事情。问题是在这reflexivity一步之后，我希望看到上下文

但我实际上得到的是

尽管这个定理仍然可以证明，但看到假设神秘地消失是令人不安的。我想知道如何获得我最初期望的上下文。从网络搜索中，我了解到这是对 Coq 中构造术语进行归纳的一般问题。关于 SO 的一种建议解决方案建议使用remember保留假设的策略。但是当我在这个证明中尝试这样做时，

induction我在步骤中收到以下错误消息。

我不太明白。我认为问题在于它E有一个自由变量，但在那种情况下我会被卡住，因为没有E引入n. （generalize dependent n会用它来概括E）

有没有办法获得最初预期的上下文？