问题标签 [theorem]

我试图在我的程序中找到一个解决方案（修复错误），它必须从定义中计算二项式定理。首先，我创建了“阶乘”-“silnia”的定义。

1) 算法确定定义的SN1(n,k)的值。（牛顿函数）

2) 算法通过公式递归确定SN3(n,k)的值。（newton_rek函数）。

输入： 文件名：In0101.txt

OUTPUT： 文件名：Out0101.txt 在这个文件中我想保存从公式计算出来的值。

示例： In0101.txt

Out0101.txt

还有一个我无法修复的错误。有人可以帮我吗？

我的代码：

我试图在 Coq 中证明一个定理，但我无法解决出现的问题。我正在尝试解决：

我是 Coq 的新手，所以我不知道这到底意味着什么。我在互联网上做了一些研究，但我没有设法找到解决方案。有谁知道这个问题来自哪里？

我正在为 OTTER 编写一个非常简单的输入文件：

我得到这个搜索输出：

为什么 OTTER 不推断Causes($c2,$c1)？

编辑：我删除了方括号[Nipah(x) & Encephalitis(x)]，它起作用了。为什么这很重要？

如果有人可以帮助我解决几个问题，我将不胜感激，

对于以下每个递归函数定义，使用主定理确定其渐近增长顺序（即 Big-Tetha）。如果您认为 Master 定理不适用于某种情况，请正确解释原因。在这些情况下，您还能为运行时间提供一个合理的上限（即 Big-O）吗？请注意，基本情况都假定为常数。

(a) T (n) = T(n/2) + 2^n

(b) T (n) = 4T(n/2) +(n^1.5) - 1

(c) T (n) = T(n/3) + 100

(d) 是 T(n) = 125T(n/5) + n^3/logn

(e) T (n) = 2T(n/7) + log n + √n

我刚刚在网上阅读了一些关于此的内容，但我无法获得足够的理解来回答这个问题。任何帮助将不胜感激，我正在努力学习考试，但我没有得到任何帮助！

非常感谢！

在我们的软件验证模块中，我们刚刚从真值表转向自然演绎。真值表看起来很基础，但现在我们使用 coq 定理证明器来证明更复杂的陈述。让我感到困惑的是，我们如何最终得到一种“已证明或未证明”类型的答案，当使用真值表时，我们可以根据输入得到真或假类型的结果，这是否意味着我们使用自然演绎来查看对于重言式，还是我完全错过了什么？

我正在尝试在 Eclipse IDE中使用 Z3 ( http://z3.codeplex.com/ )。我安装了 PyDev 并下载了 Z3 的预编译 Windows 二进制文件。我还将“bin”子目录添加到环境变量 PYTHONPATH 和 PATH 中。

在这个非常简单的例子中，

Eclipse 说 Real e Solver 是未定义的变量。运行此代码我收到此错误消息：

“ImportError: Bad magic number in ...\bin\z3.pyc”

似乎这是与解释器不同的python版本（通常较晚）的问题（请参阅：What's the bad magic number error？）。

有什么帮助吗？我是否需要编译和安装 Z3Py 而不是使用预编译的 Windows 二进制文件？

谢谢。

我试图证明这个引理

但是另一个功能 reverse-helper 不断出现在我的目标中，我不知道如何摆脱它。有什么指导或建议吗？

I'm stuck on a lemma "left as an exercise" from this lecture. It goes like this:

Where even is an inductive predicate defined like this:

Help, please? I always end up with (S (S p) = 2 or similar.

EDIT

Some lemmas and tactics I used (not complete proof):

我从 Isabelle 的维基百科页面获得了以下代码：

但是，当我将此文本复制到 Isabelle 实例中时，每行左侧有多个“请勿输入”符号。有人说“在顶层非法应用命令“定理””，所以我假设你不能简单地在顶层定义一个定理，并且维基百科页面没有提供完整的初始示例。我将定理包装在一个理论中，如下所示：

伊莎贝尔不再抱怨这个定理，但是，在定理的第二行，它现在说：

它还抱怨证明线：

对于定理中的其余行，它也有错误。包装维基百科提供的这个定理以便可以在 Isabelle 中检查的正确方法是什么？

我正在尝试实现四色定理。四色定理指出，平面上的任何地图都可以使用四色着色，使得共享共同边界的区域（除了单个点）不共享相同的颜色。有一个分成区域的地图，这些区域被放入一个邻接矩阵中，通过使用四种颜色，我试图为地图着色，以便没有两个连续的区域共享相同的颜色。邻接矩阵用于编码哪个区域与另一个区域接壤。矩阵的列和行是区域，如果两个区域不相邻，则单元格包含 0，如果它们有边界，则包含 1。

编辑 它必须是递归的

我使用的邻接矩阵是：

我被困在哪里去。提前感谢您的帮助。

这是我的代码：