FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

01.11
Sat
おはようございます〜

今日から大学の長期休みです〜!やったね!


さてさて、自動定理証明っぽいの書いてみました

バイナリは用意してないので動かすには

なんらかのCommon Lisp処理系(SBCL or CLISPを想定していますが)が必要です

ソースは git clone https://github.com/moratori/lexpr.git で

$ sbcl --script main.lisp #or
$ clisp main.lisp

で動くとおもいます

起動してみると

$ sbcl --script main.lisp
Theorem Prover Beta 0.9

Input set of wff {
?

こんな感じになるので、論理式を書いていきます。まず有名な例(ソクラテスが死ぬやつ)をやってみます.


この場合ソクラテスが死ぬかどうか判定するには、2つの前提が必要です.つまり

 (全ての人間は皆死ぬ運命です!という意味)

 (ソクラテスは人間ですという意味)

このふたつです。この時僕らは確かに、あぁソクラテスは死ぬんだなぁと理解するわけですが

これをやってみると以下の感じになります。

Input set of wff {
? Ax.( human(x) > mortal(x) )
inputted: ∀x.human(x)⊃mortal(x)
? human(socrates)
inputted: human(socrates)
? }
conseq ? mortal(socrates)
inputted: mortal(socrates)

まず前提2つを入力します。全称量化子は大文字のAです。ちなみに存在量化子は大文字のEです。逆なので注意です

一つ式を入力するとinputted: hogehogeみたいな感じで、どのように式が解釈されたのかがエコーされます

で前提の終わりには、 } を入力します

最後に conseq? で結論を聞かれます。つまりこの場合 mortal(socrates) を入力します

すると、この mortal(socrates) は確かに前提の論理式から導かれるものなのか否かを確認してくれます。

で、このようになります

{human(socrates) , ∀x.human(x)⊃mortal(x) , ¬mortal(socrates) , } is contradiction
{human(socrates) , ∀x.human(x)⊃mortal(x) } |= mortal(socrates)

output to TeX? (y or n)


{hoge} is contradiction
{hoge} |= foo

みたいな表示になったら、たしかに結論となるということがわかります

で、この場合タブロー木をTeXファイルに出力することができます。
(TeXファイルをコンパイルする時はecltree.styが必要になります)

こんな感じになります

Screenshot from 2014-01-11 07:45:19



ではもう少し複雑な例をやってみます

前提となる論理式を以下とします


 
(全てのハンサムな男性には彼女がいる)


(カップルである人たちはみんな幸せです)

そして結論を以下とします


(ハンサムな男性は幸せいっぱいです)


これを入力すると、たしかに論理的に正しいことがわかります

Screenshot from 2014-01-11 08:11:29



RE-643とかRE-644とかいうのは推論の過程でつかわなきゃいけないシンボルです.

意味はありません気にしないでください


(定理証明とか言っといて、定理証明してなかった...)


ちなみに初期のAI研究なんかはこのように

人間の知識や推論を離散的な記号データで形式化して表そうとしたわけです。

Prologなんかは典型なわけです
スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/181-437016f9
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。