嗨，大家好，我試圖比較2個算法，並認爲我可能會嘗試爲他們寫一個證明！ （我的數學很爛所以因此問題）寫一個算法的證明
通常，在去年我們的數學課，我們將給予像
一個問題證明：（2R + 3）= N（N + 4）
然後我會做所需的4個階段，並在最後得到答案
我在哪裏卡住證明prims和克魯斯卡爾斯 - 我怎樣才能得到這些算法在形式像上面的數學一樣，所以我可以着手證明
注意：我不是要求人們回答疫情週報對我來說 - 只要幫我把它在一個形式，我可以有一個自己去
感謝
你不給許多細節，但有數學家的社區（數學知識管理MKM）他們開發了支持計算機數學證明的工具。參見，例如：
，並在統一I（隱約）最新的會議
從我的數學課記得Prims證明和Kruskals算法 - 你不攻擊它通過以數學形式寫它。相反，您對圖形採用成熟的理論，並將它們結合起來，例如http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness來建立證明。
如果你想證明覆雜性，那麼簡單地通過算法的工作就是O（n^2）。對於圖表稀疏的特殊情況有一些優化，可以將其減少到O（nlogn）。
我在哪裏卡住的prims和Kruskals證明 - 我怎麼能到像工科數學一個以上這樣我就可以繼續處理的形式獲得這些算法來證明
我不認爲你可以做到直。相反，證明兩者都生成一個MST，然後證明任何兩個MST是相等的（或等價的，因爲對於某些圖可以有多個MST）。如果兩種算法都生成顯示爲等效的MST，則算法是等效的。
爲了證明算法的正確性，您通常必須顯示（a）它已終止，並且（b）其輸出滿足您要執行的操作的規範。這兩個證明與您在問題中提到的代數證明有很大不同。您需要的關鍵概念是mathematical induction。 （樣本爲recursion）
以quicksort爲例。
爲了證明快速排序總是終止，你首先表明它終止了長度爲1的輸入（這是平凡true），則表明，如果它終止了長度達輸入ñ，然後它會終止輸入長度n + 1。歸功於感應，這足以證明算法終止所有輸入。
爲了證明quicksort是正確的，您必須將比較排序規範轉換爲精確的數學語言。我們所要的輸出是輸入這樣的permutation，如果我 ≤ Ĵ然後一個我 ≤ 一個Ĵ。證明quicksort的輸出是輸入的排列很容易，因爲它從輸入開始並交換元素。證明第二個屬性有點棘手，但是你也可以使用歸納。
大多數情況下，證明取決於您手中的問題。 簡單的說法有時可以滿足，在其他一些時候你可能需要嚴格的證明。我曾經用一個推論和證明已證明的定理來證明我的算法是正確的。但那是一個大學項目。
也許你想嘗試一種半自動證明方法。 ）例如，如果您有Prim's和Kruskal算法的Java規範，最佳地建立在相同的圖形模型上，則可以使用KeY Prover來證明算法的等價性。
關鍵的部分是在動態邏輯（這是一階邏輯的擴展，符號執行Java程序的方式）的形式化證明義務。爲了證明該公式能夠符合下列（粗略）模式：
\forall Graph g. \exists Tree t.
(<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)
這表示，對於所有的圖，這兩種算法終止，結果是一樣的樹。
如果你很幸運，你的公式（和算法實現）是正確的，那麼KeY可以自動爲你證明它。如果不是，您可能需要實例化一些量化變量，這使得有必要檢查先前的證明樹。在KeY證明了這件事之後，你可以開始學習某些東西或者嘗試從KeY證明中重構一個手工證明 - 這可能是一個單調乏味的任務，因爲KeY知道很多Java特有的規則，不容易理解。然而，也許你可以做一些事情，比如從KeY用於在證明中的後綴右邊實例化存在量詞的術語中提取Herbrand分解。
嗯，我認爲關鍵是一個有趣的工具，更多的人應該習慣使用證明這樣的工具，關鍵Java代碼）
如果你已經在KeY中證明了Prim或Kruskal的算法，我想看看它！我只是不相信任何證明助理都適合這樣的事情。 – user21820 2014-04-24 17:27:23
嘗試mathoverflow.com。我想你會有更多的運氣 – Toad 2009-12-23 10:57:21
我不認爲這種問題是什麼mathoverflow.com是。 – 2009-12-23 14:46:19