Fitch 形式 ( Language, Proof and Logicで使用) を使用して、特定の一連の前提と目標を設定し、問題を解決するために必要な手順の完全なリストを表示できるソフトウェアはありますか?
質問する
16016 次
3 に答える
7
于 2011-12-29T14:29:31.827 に答える
5
簡単な答え: いいえ。
中程度の回答: 実際にはできませんが、与えられた証明の有効性をチェックするプログラムをかなり簡単に作成することはできます。命題論理の場合、証明を自動的に見つける問題は NP 完全であり (決定可能ですが!)、一階論理には、証明者が停止しない真の定理があります。(決定不能) (ゲーデルの不完全性証明による)
そのようなことを書くことに興味がある場合は、それを試してみて、いくつかの小さなケースで動作させることができますが、一般的には実行できません.
宿題の答えを得るためにそのようなものを探しているなら、やめてください。(a) あなたはそれを見つけることができず、(b) その本の問題はとても簡単で、楽しいものです! 試してみて、必要に応じて助けを求めてください。もちろん、(c) カンニングをしても何も学べません。
于 2010-06-29T10:38:12.740 に答える
0
OLI Carnegie Mellon http://www.phil.cmu.edu/projects/apros/による Apros を検討してください。
于 2014-11-29T09:22:53.653 に答える