結果として自分がIsabelleを咀嚼するのはまだかかりそうだという感想だったが、もっと初歩的なことをやって練習していくことにしたい。題材としては論理学の教科書に出てくるような自然演繹による証明をIsabelleでやってみることにする。R」のように前提P,Q,...から帰結Rが出てくるものとするとP,Q,...に対してあらかじめ用意されたルールを適用して変形することで最終的にRが出てくれば証明完了というものだ。Isabellの証明はtheoryという構造の中に書く。jEditで次のようなファイルを作ってNaturalDeduction.thyというファイル名で保存する。*)endファイル名とtheoryの名前は一致しなければならない。jEditは特に拡張子を自動でつけてくれないが、拡張子がないと証明ファイルとして認識されないので注意しなければならない。Main"とは何か、はよくわかっていないが気にしないことにする。<stdio.h>のようなものだろう。コメントはMLスタイルで、「(*」と「*)」で囲む。Q∩R"を証明してみよう。Science"から採っている。これを証明するにはまずP∩QからQを取り出し(P∩Qが成立するということはQ単独でも成立する)、QとRからQ∩Rを作る(QとRが成立するということはQ∩Rも成立する)必要がある。問題はIsabelleでそのようなルールが何という名前で提供されているかだが、既存の定理を探すにはfind_theoremsというコマンド(?)を使う。_"このように書くと検索結果の最初のほうに出てくるconunct2とconjIが求めているものだとわかる。Q∩R"という定理を表明するにはこのように書けばいいようだ。R"つまり前提をassumes、帰結をshowsのところに書く。"R"と書いてもいいようだ。Qは「任意のPとQをとった時に」という意味だがこれは書かなくても暗黙の裡にそうなるそうだ。「1:」とかいうのは前提などに後で使うための名前を付けている。これだけだと問題を表現しただけで、証明ではない。証明は続けて書くのだが、こうなる。conjI)qedproofのあとにハイフンをつけるのは...なんだっけ。セミナーで説明してもらったと思うのだがあまり理解できず、忘れてしまった。この例ではハイフンを消すとエラーになる。前提からこういう事実が導けますというのをhaveとかshowで宣言する。haveとshowの違いは、途中に来るのがhaveで最後に来る(証明したかった)ものがshowだと考えればよいようだ。conunct2)になる。usingがIsabelle的にどういう機能なのかきちんと理解していないのだが、とりあえずこの例ではルールの引数を指定するようなイメージのものだと解釈できる。3と2を使ってconjIを使うと4が出せる。subgoals!となる。subgoals!になったらそこにqedと書く」と思っておけばよいようだ。次に二重否定の除去(~~PからPを導く)と導入(Pから~~Pを導く)を扱う例を書きたい。auto検索により二重否定の除去はnotnotDが使えるとわかる。二重否定の導入は見つからなかったので独自に定理として作る。autoで自動的に証明できてしまうのだが、それがなぜかは気にしないことにする。~~P∩R"の証明が書ける。tollensを使った証明をしたい。いずれもそのものはIsabelleの中にないようなので定理として作っておく。~Q"はMPとMTを順に適用することで証明できる。mt)qed次は==>を導入するような式変形ルールを使う。これはいままでのルールとはちょっと違って「Pを仮定したときにQが導けるならばP==>Qを導いてよい」というものだ。P⇒~~Q"を証明する例が次のものだ。mt)qed==>がいくつもあるような証明を行うときは入れ子構造になる。⟹(P⟹R))"ということである。いままでhaveやshowで宣言した式の証明をするのにbyを使ってきたが、ここではbyの代わりに入れ子のproofを書いている。上の例はフラットに書いても同じことができる。やったので今度は選言を使う。選言には「PがいえるならばP∪Qも言える」というもの(導入)と、「P∪Qが言えて、Pの場合とQの場合でいずれもRが導けるならば、Rを導いてよい」(除去)の2つがある。前者はIsabelleに既にあり、後者はなかったので独自の定理を作る。P∪R"の証明が書ける。qedqed次に"P⟹(Q⟹P)"を証明することを考えてみる。この場合Pは前提としているんだからQは関係なくPを前提しているということからそのままPが出てくるはずだ。(2004)ではこのルールをcopyと呼んでいる。assupmtion」と書けばいいようだ。qedqed次の証明では「Pと~Pが両方出てきたら矛盾している」と例の「矛盾からは何でも出てくる」を使う。前者はnotE、後者はFalseEとしてIsabelleで用意されている。disjE)qed最後に「Pと仮定して矛盾が導かれるならばPではない(~Pを導ける)」を使う。これはIsabelleではnotIという名前である。notI)qed以上Isabelleで命題論理の自然演繹の証明をいくつか書いてみた。「~のようだ」が多い記事になったことは申し訳なく思う。コメント(0)あなたは既にnice!を行っています。一定件数以上前のnice!は表示されませんのでご了承ください。0コメントを書くコメント投稿に失敗しました。未入力の項目があります。認証コードが一致しませんでした。半角英数字のみのコメントは受け付けできません。お名前:URL:コメント:画像認証:下の画像に表示されている文字を入力してください。(..単体テストのための外部DSLカテゴリーOCaml(62)Tcl(27)D言語(5)COM(1)PowerShell(9)JavaScript(5)Linux(2)Lua(19)XSLT(1)Lisp(32)Excel(2)コードリーディング(4)Ruby(9)言語比較(7)Haskell(6)Groovy(1)PHP(10)Scala(48)Perl(2)Erlang(4)Python(2)Prolog(8)Java(8)自然言語(1)awk(1)SML(19)sh(2)SMV(1)YokohamaUnit(8)Rehearsal(1)Isabelle(1)最近のコメント不本意というよりは意外、というのが..ご案内ありがとうございます。..ご紹介&コメントありがとうございま..OCaml3.11のCamlp4か..エラー出た時はここが参考になりまし..コメントありがとうございます。SML#のバグ報..コメントありがとうございます。ソネットポイントこの広告は前回の更新から一定期間経過したブログに表示されています。更新すると自動で解除されます。この広告は180日新規投稿のないブログに表示されます。