私は 2 年生で、離散数学 2 の課題は自動定理証明器を作成することです。命題論理で動作する単純な証明プログラムを 4 週間で作成する必要があります (証明が常に存在すると仮定して)。これまでググってきましたが、そこにある資料は 4 週間で理解するのが本当に難しいです。初心者向けの本/サイト/オープンソースコードや、始めるのに役立つヒントを教えてくれる人はいますか? 前もって感謝します。
質問する
2219 次
1 に答える
3
注: 私はこれをコンピューター サイエンス サイトに移動するようにフラグを立てました。
あなたが見たものと、それが役に立たない理由を含めていただければ幸いです. それから、私たちはあなたにとって何がより良いかを理解することができます. また、プログラムを作成する必要がある場合は、知っている言語を知っておくと役立ちます。私がこれで行うことのほとんどは、OCaml や F# などの関数型言語、または Prolog や Mercury などの論理言語で行われます。
ジョン・ハリソン著の「実践的論理と自動推論のハンドブック」(WorldCat)を見たことがありますか? （WorldCat）リンクを含めたので、ほとんどの時間を費やすことになる本を購入するのを待つのではなく、地元の図書館で本を見つけることができます.
ページの一番下にOCamlのコードがあり、F#はこちら、Haskellはこちらです。
ウィキペディアでATPやProof Assistantを見たことがない場合は、コードや論文にたどり着くかもしれません。
于 2013-02-19T22:49:42.470 に答える