我正在尝试比较两种算法。我想我可以试着为他们写一个证明。（我的数学很烂，所以这个问题。）
通常在我们去年的数学课上，我们会遇到一个问题，比如 <can't use symbols in here so left them out>。
证明： (2r + 3) = n (n + 4)
然后我会完成所需的 4 个阶段并在最后得到答案。
我被卡住的地方是证明 prims 和 Kruskals - 我怎样才能将这些算法转化为上述数学算法的形式，以便我可以继续证明？
注意：我不是要求人们为我回答 - 只是帮助我把它变成一个我可以自己去尝试的形式。
为了证明算法的正确性，您通常必须证明 (a) 它终止和 (b) 它的输出满足您尝试执行的规范。这两个证明将与您在问题中提到的代数证明有很大不同。您需要的关键概念是数学归纳法。（这是证明的递归。）
我们以快速排序为例。
为了证明快速排序总是终止，您首先要证明它会因长度为 1 的输入而终止。（这很简单。）然后证明如果它因输入长度不超过n而终止，那么它将因输入长度为 n而终止+1。由于归纳，这足以证明算法对所有输入都终止。
要证明快速排序是正确的，必须将比较排序的规范转换为精确的数学语言。我们希望输出是输入的排列，如果i ≤ j则a i ≤ a j。证明快速排序的输出是输入的排列很容易，因为它从输入开始并且只是交换元素。证明第二个属性有点棘手，但您可以再次使用归纳法。
您没有提供太多细节，但有一个数学家社区（数学知识管理 MKM）开发了支持数学计算机证明的工具。参见，例如：
和最新的会议
我被卡住的地方是证明 prims 和 Kruskals - 我怎样才能将这些算法转化为上述数学算法的形式，以便我可以继续证明
我不认为你可以直接。相反，证明两者都生成一个 MST，然后证明任何两个 MST 相等（或等价，因为对于某些图，您可以有多个 MST）。如果两种算法都生成的 MST 被证明是等价的，那么这些算法是等价的。
大多数情况下，证据取决于您手中的问题。有时简单的论证就足够了，有时你可能需要严格的证明。我曾经使用已经证明的定理的推论和证明来证明我的算法是正确的。但这是针对大学项目的。
From my maths classes at Uni I (vaguely) remember proving Prims and Kruskals algorithms - and you don't attack it by writing it in a mathematical form. Instead, you take proven theories for Graphs and combine them e.g. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness to build the proof.
If your looking to prove the complexity, then simply by the working of the algorithm it's O(n^2). There are some optimisations for the special case where the graph is sparse which can reduce this to O(nlogn).
也许您想尝试一种半自动证明方法。只是为了不同的东西；）例如，如果您有 Prim 和 Kruskal 算法的 Java 规范，并以最佳方式构建在相同的图形模型上，您可以使用Key Prover来证明算法的等价性。
关键部分是在动态逻辑中形式化您的证明义务（这是一阶逻辑的扩展，具有 Java 程序的符号执行类型和方法）。要证明的公式可以匹配以下（粗略）模式：
\forall Graph g. \exists Tree t.
(<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)
这表示对于所有图，两种算法都终止并且结果是同一棵树。
如果您很幸运并且您的公式（和算法实现）是正确的，那么 KeyY 可以自动为您证明。如果没有，您可能需要实例化一些量化变量，这使得有必要检查先前的证明树。
在用 KeyY 证明了这件事之后，你可以很高兴学到了一些东西，或者尝试从 Key 证明中重建手动证明——这可能是一项乏味的任务，因为 KeyY 知道很多 Java 特有的规则，这些规则并不容易理解。然而，也许你可以做一些事情，比如从 Key 用来实例化证明中序列右侧的存在量词的术语中提取 Herbrand 析取。
好吧，我认为 KeyY 是一个有趣的工具，应该让更多的人习惯使用这样的工具来证明关键的 Java 代码；）