- 从哪里开始？

我是一名二年级学生，拥有离散数学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

- 从哪里开始？

回答

相关问题