问题标签 [theorem]

我知道 Dijkstra 的算法是如何工作的，并且它可以在 O(m + n log n) 时间内运行。我们怎么知道没有比这更好的单源最短路径算法了？

如何将以下问题解决为 f(n)=n! 据我所知，不适用于主定理的任何情况。T (n) = 16T (n/4) + n！

我正在学习算法设计课程，我有一个计算函数成本的作业，我做了一些研究并发现了主定理，但我看到的所有例子都是关于n的，在这个函数中我有 2 个参数，但都没有是 n。

我们知道 resulta(x,y) 是 O(1)，但是我如何计算具有 2 个参数 i 和 j 而不是 n 的主定理的递归函数的成本？是不可能的，我必须使用替换方法？

我正在开发一阶逻辑模型。我想证明它是一致的。可能吗？我可以使用任何免费工具来执行此操作吗？

或者由于哥德尔定理这是不可能的？

此致。

正如标题中所写，我的问题是关于创建一个程序的可能性，该程序在给定假设和论文的情况下，尝试以某种方式演示该定理并在可证明的情况下打印给用户。

我使用 bookdown 生成 html 和 PDF 格式的文档。如何在定理和示例环境中使用内联 R 代码的结果？

这是我尝试过的：

我得到

这是关于实现数学定理的一般设计问题。我正在尝试用编程语言从微分几何中实现一些数学定理（无论哪种都无所谓；为简单起见，我使用python语言，但这不应该影响一般思想。）。我可以用一个例子更好地描述这个问题。

定理： r>= 2 类曲面上的任何直线都是渐近曲线。

如何实现这样的定理。显然，该函数需要一条线作为参数，而曲面作为参数。

函数应该只返回真、假还是不可判定？或者该函数是否应该返回“渐近”。如果我们将函数命名为“is-asymptotic”，那么它应该返回 true、false 或 undecidable。

函数应该检查的第一件事是线是否是直的。让我们不要深入细节。然后，它应该计算表面的类别

上述方法促使我返回真/假。另一方面，如果我将它实现为一个名为 line 的类的方法，它要求给定 line 的所有属性，那么它应该返回一个属性列表，包括“渐近”。

最后，我在上面所做的是要求给定行的属性，即我们的论点。该函数没有说明所有其他直线。

您将如何解决定理的整个实现设计？

先感谢您。

PS。为了进一步阐明编程语言内容中的问题，将上述问题改写如下。假设我有一个对象“Line”的实例“line”。我是否询问实例是否是渐近的，如

还是我要询问它的属性并获取包含渐近属性的属性列表，如

或者在创建实例时，在检查它是否是直的之后，我将属性设置为渐近线，如

我编写了一个函数，该函数应该使用威尔逊定理检查整数是否为素数。然而，它输出 5 不是素数，这显然是。我想问这是为什么？

Z3 如何返回一个有效的反例？以下代码

输出counterexample []。

我不必使用prove，但我想为f示例中的公式找到一个有效的反例。我该怎么做？

我想用我能想到的Mizar数学定理证明器语言编写最简单的证明。所以我想到了以下几点：

存在 x \in Nat : x = 1

没有什么比我能想到的更简单的了。我给了它以下尝试：

但正如你所见，Mizar 不喜欢我的证明。我错过了什么？

这仍然不起作用：