…にするだけではダメ「Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか」より引用： ここ数年のウェンツェルの主張を追ってみると、Isabelleの世界を広げようと尽力しているのが分かります。証明支援系の利用が広がらないネックは、「難読な証明記述言語と貧弱なユーザーインターフェースだ」との認識のもと、Isar（Isabelleの宣言的証明記述言語）とIsabelle/jEditにより障壁を取り除く戦略のようです。 ウェンツェル〈Makarius Wenzel〉…

…ースに、Mizar、Isabelle/Isar、ラムダ項の各種シンタックスシュガーなどを参考にしたものです。使用するキーワードこの記事で説明するキーワードを出現順に列挙します。 $`\have`$ $`\need`$ $`\letsShow/\: \conclude`$ $`\theorem/\: \proof /\: \qed`$ $`\par/\:\endBlock`$ $`\case/\:\endBlock`$ $`\assume /\: \endBlock`$ $`\…

…hree.html Isabelle ：https://behemoth.cl.cam.ac.uk/search/ Lean 4 ： https://leanprover-community.github.io/mathlib4_docs// 検索ツールがあるとは言いながら、ソースコード内を文字列検索する原始的方式なので、意図している目的の定理にたどり着くのは容易ではありません。最も有効で手っ取り早い検索手段は、よく知っている人に聞くことです。チャットAIは「よく知っている人…

…自然言語を解釈しながら翻訳作業をする必要があるところです。手動トランスパイルは人間（僕）がやっているので、自然言語解釈は問題ありません（そりゃそうだ）が、自然言語処理とプログラミング言語処理が混じった翻訳系を作るのはチャレンジングかも知れません。いやっ、意外とアッサリできちゃうかも ‥‥？ どうだろ？ ウーン、よくわからんです。 *1:Lean 4の場合、Isabelle/Isarのような別言語があるわけではなくて、ラムダ式に対する薄いシンタックスシュガーが少数あるだけです。

…の一般的知識、さらには証明論まで勉強して」という意味合いです。 *4:困った問題点があってもタクティク証明が主流なのは、短いスクリプトでコンパクトに書けて、アルゴリズム化がしやすく、自動証明にも容易に繋がるからです。 *5:MizarやIsabell/Isarは、人間可読な直接証明記述を目指したソフトウェアです。Isabell Isar のブログ内検索結果 参照。タクティク証明に比べて、直接証明のソフトウェア支援は設計・実装が困難という事情もあって、主流になれないのでしょう。

…と思います。CoqやIsabelleとは比べものにならないくらい読みやすいです。 構文や意味モデルはホントに素晴らしいんですよ。ソフトウェアとしては「こんなもん使えるか！」と投げ出すレベルなんですが、CoqやIsabelleでは代替できない機能と用途を持っているので、フラストレーションに耐えながら調べたり試したりしています。MizarコミュニティMizarは、1970年代初頭に、アンジェイ・トリブレッツ*2（Andrzej Trybulec 1941-2013）がMS-DOS…

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界「Isabelle/jEditの野心的な試み「継続…

…す。今日話題にしたいIsabelle（イザベル）は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています（Coqもほぼ同時期にスタートしています）。十分に枯れた処理系でありながら、現在でも開発は活発で、新しい地平に向けて果敢な挑戦も試みられています。特に、ユーザーインターフェースの改善に熱心で、現在のGUIフロントエンドであるIsabelle/jEditには、驚くべき機能（の卵）が実装されています。内容： 継…