- 從哪裏開始？

我是一名二年級學生，擁有離散數學2項任務是製作自動化的定理證明。我必須在4周內製作一個適用於命題邏輯的簡單證明程序（假設證明總是存在）。我已經搜索了很多東西，但是這些材料在4周內真的很難理解。任何人都可以推薦我一些書籍/網站/開源代碼，爲初學者或一些有用的提示開始？先謝謝你。- 從哪裏開始？

來源

2013-02-19 minhnhat93

注意：我將此舉標記爲轉移到計算機科學網站，因爲它們比那裏的ATP更重要。

如果你可以包括你所看到的以及爲什麼它不能幫助你，那將是很好的。然後我們可以弄清楚什麼可能對你更好。另外，如果你必須編寫一個程序，那麼知道你知道什麼語言將會有所幫助。我所做的大部分工作都是用OCaml或F＃等函數式語言或Prolog或Mercury等邏輯語言完成的。

你見過約翰哈里森的「Handbook of Practical Logic and Automated Reasoning」(WorldCat)。我包括了(WorldCat)鏈接，所以你可以在當地的圖書館找到這本書，而不是等待購買它，這會消耗掉大部分時間。

如果你看，你會發現在頁面底部的OCaml代碼，和F＃here和Haskell here。

如果你還沒有在維基百科看到ATP或Proof Assistant，你可能會得到一些代碼和論文。

來源

2013-02-19 22:49:42

感謝您的開源鏈接，但我不知道F＃和Haskell和OCaml，所以我認爲我會堅持使用C++。無論如何，我在http://arxiv.org/ftp/cs/papers/9301/9301110.pdf找到了一個有趣的傢伙。我想我會和他一起玩一會兒。 – minhnhat93 2013-02-20 03:29:35

@ minhnhat93好紙。保爾森在這個問題上是最好的領域之一。您知道示例代碼是ML，它是一種功能語言，是OCaml和F＃的前身？如果你能得到Paulson的「ML for the working programmer」，它應該可以幫助你更好地理解代碼。 – 2013-02-20 04:48:11

是否有任何特別的原因，這些證明書大部分是用函數式語言編寫的，而不是用c，java，c＃等流行語言編寫的？如果ML是OCaml和F＃的前身，那麼我想我現在需要學習F＃。 – minhnhat93 2013-02-20 06:36:07

- 從哪裏開始？

回答

相關問題