これを証明できる自動定理証明システムを探しています。
クロコダイルは男の子供を連れて行きました。男はワニに自分の子供を食べないように頼んだ. しかし、クロコダイルは言いました。
彼の分析ソリューションは次のようになります。
x - ワニは子供を食べる y - 男性 答え: ワニは子供を食べる
~ は等しいことを意味します。意味しない、-> 意味する、+ OR;
((x~y)->!x) and ((x XOR y)->x) =
(x! and y +!x and y+!x)(!x!y+x and y+x) =
(!x+!y)(x+!y) = !y;
ですから、答えは男性が言わなければならないということです：「あなたは子供を食べるつもりはありません」。
さて、ここにはたくさんのシステムがリストされています: http://en.wikipedia.org/wiki/Automated_theorem_proving
私はそれらのうちの5-6を試しましたが、ここで何をしているのか本当に理解できませんでした. この定理をそれらの中で形式化して、その最初の部分に入ることができるようにする方法:
((x~y)->!x) and ((x XOR y)->x)
そして答えを得る
y出力として。
少なくともどのシステムが自動的にそれを行うことができるか、さらにヒントを教えてください。
よろしく、コンスタンチン。